Dave is red. Harry is big. Harry is blue. All young, round things are blue. If Harry is round then Harry is cold. If Dave is big and Dave is young then Dave is round. If Harry is cold then Harry is white. Blue, young things are white. If something is big then it is cold.
Dave is red.
("Dave" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
All young, round things are blue.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
If Harry is round then Harry is cold.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "cold" "+"))
If Dave is big and Dave is young then Dave is round.
((("Dave" "is" "big" "+") ("Dave" "is" "young" "+")) -> ("Dave" "is" "round" "+"))
If Harry is cold then Harry is white.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "white" "+"))
Blue, young things are white.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
If something is big then it is cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
Harry is blue.
True
1
proof
[(triple3)]
("Harry" "is" "blue" "+")
triple3
Dave is not red.
False
1
inv-proof
[(triple1)]
("Dave" "is" "red" "-")
triple1
Harry is cold.
True
2
proof
[(((triple2) -> rule6))]
("Harry" "is" "cold" "+")
((triple2) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple2) -> rule6))]
("Harry" "is" "cold" "-")
((triple2) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
True
3
proof
[(((((triple2) -> rule6)) -> rule4))]
("Harry" "is" "white" "+")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not white.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule4))]
("Harry" "is" "white" "-")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "cold" "-")
Dave is round.
Unknown
rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "round" "+")
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "blue" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Dave is red.[(triple1)] Harry is big.[(triple2)] Harry is blue.[(triple3)] @1: Harry is cold.[(((triple2) -> rule6))] @2: Harry is white.[(((((triple2) -> rule6)) -> rule4))]
Dave is red.
("Dave" "is" "red" "+")
triple1
Harry is big.
("Harry" "is" "big" "+")
triple2
Harry is blue.
("Harry" "is" "blue" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
((triple2) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2