Charlie is red. Dave is cold. Dave is white. Gary is furry. Harry is quiet. Harry is red. Harry is young. Cold things are furry. All red, young things are furry. All white, red things are young. All cold, red things are young. Red, quiet things are cold. All red things are cold. If Gary is red then Gary is big. If something is big and cold then it is young.
Charlie is red.
("Charlie" "is" "red" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is young.
("Harry" "is" "young" "+")
Cold things are furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
All red, young things are furry.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
All white, red things are young.
((("something" "is" "white" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
All cold, red things are young.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
Red, quiet things are cold.
((("something" "is" "red" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
All red things are cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If Gary is red then Gary is big.
((("Gary" "is" "red" "+")) -> ("Gary" "is" "big" "+"))
If something is big and cold then it is young.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
Charlie is red.
True
1
proof
[(triple1)]
("Charlie" "is" "red" "+")
triple1
Dave is not cold.
False
1
inv-proof
[(triple2)]
("Dave" "is" "cold" "-")
triple2
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "big" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Charlie is red.[(triple1)] Dave is cold.[(triple2)] Dave is white.[(triple3)] Gary is furry.[(triple4)] Harry is quiet.[(triple5)] Harry is red.[(triple6)] Harry is young.[(triple7 OR ((((triple6) -> rule6) triple6) -> rule4) OR ((((triple6 triple5) -> rule5) triple6) -> rule4))] @1: Charlie is cold.[(((triple1) -> rule6))] Dave is furry.[(((triple2) -> rule1))] Harry is cold.[(((triple6) -> rule6) OR ((triple6 triple5) -> rule5))] Harry is furry.[(((triple6 triple7) -> rule2) OR ((((triple6) -> rule6)) -> rule1) OR ((((triple6 triple5) -> rule5)) -> rule1) OR ((triple6 ((((triple6) -> rule6) triple6) -> rule4)) -> rule2) OR ((triple6 ((((triple6 triple5) -> rule5) triple6) -> rule4)) -> rule2))] @2: Charlie is furry.[(((((triple1) -> rule6)) -> rule1) OR ((triple1 ((((triple1) -> rule6) triple1) -> rule4)) -> rule2))] Charlie is young.[(((((triple1) -> rule6) triple1) -> rule4))]
Charlie is red.
("Charlie" "is" "red" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is white.
("Dave" "is" "white" "+")
triple3
Gary is furry.
("Gary" "is" "furry" "+")
triple4
Harry is quiet.
("Harry" "is" "quiet" "+")
triple5
Harry is red.
("Harry" "is" "red" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
((((triple6) -> (rule6 % int2)) triple6) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple6 triple5) -> (rule5 % int2)) triple6) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple1) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple2) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple6) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple6 triple5) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple6 triple7) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple6 triple5) -> (rule5 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((triple6 ((((triple6) -> (rule6 % int3)) triple6) -> (rule4 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
((triple6 ((((triple6 triple5) -> (rule5 % int3)) triple6) -> (rule4 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((triple1 ((((triple1) -> (rule6 % int3)) triple1) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
((((triple1) -> (rule6 % int2)) triple1) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2