Erin is smart. Harry is quiet. If something is quiet then it is cold. If something is smart and not rough then it is not round. If something is cold then it is smart.
Erin is smart.
("Erin" "is" "smart" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If something is quiet then it is cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
If something is smart and not rough then it is not round.
((("something" "is" "smart" "+") ("something" "is" "rough" "~")) -> ("something" "is" "round" "-"))
If something is cold then it is smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
Erin is smart.
True
1
proof
[(triple1)]
("Erin" "is" "smart" "+")
triple1
Erin is not smart.
False
1
inv-proof
[(triple1)]
("Erin" "is" "smart" "-")
triple1
Harry is cold.
True
2
proof
[(((triple2) -> rule1))]
("Harry" "is" "cold" "+")
((triple2) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple2) -> rule1))]
("Harry" "is" "cold" "-")
((triple2) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("Harry" "is" "smart" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not smart.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("Harry" "is" "smart" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Erin is not cold.
Unknown
inv-rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "cold" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
@0: Erin is smart.[(triple1)] Harry is quiet.[(triple2)] @1: Harry is cold.[(((triple2) -> rule1))] @2: Harry is smart.[(((((triple2) -> rule1)) -> rule3))]
Erin is smart.
("Erin" "is" "smart" "+")
triple1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple2
Harry is cold.
("Harry" "is" "cold" "+")
((triple2) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2