Charlie is big. Charlie is red. Dave is white. All red things are green. If something is white then it is green. If something is big and green then it is furry. All big things are green. If something is big and green then it is smart. If something is smart then it is big.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
All red things are green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If something is white then it is green.
((("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
If something is big and green then it is furry.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
All big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If something is big and green then it is smart.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
If something is smart then it is big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
Charlie is red.
True
1
proof
[(triple2)]
("Charlie" "is" "red" "+")
triple2
Dave is not white.
False
1
inv-proof
[(triple3)]
("Dave" "is" "white" "-")
triple3
Dave is green.
True
2
proof
[(((triple3) -> rule2))]
("Dave" "is" "green" "+")
((triple3) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple3) -> rule2))]
("Dave" "is" "green" "-")
((triple3) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not furry.
Unknown
inv-rconc
[@3: Dave is furry.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule5 <- FAIL)]]
("Dave" "is" "furry" "-")
Dave is big.
Unknown
rconc
[@2: Dave is big.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Dave" "is" "big" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
@0: Charlie is big.[(triple1)] Charlie is red.[(triple2)] Dave is white.[(triple3)] @1: Charlie is green.[(((triple1) -> rule4) OR ((triple2) -> rule1))] Dave is green.[(((triple3) -> rule2))] @2: Charlie is furry.[(((triple1 ((triple1) -> rule4)) -> rule3) OR ((triple1 ((triple2) -> rule1)) -> rule3))] Charlie is smart.[(((triple1 ((triple1) -> rule4)) -> rule5) OR ((triple1 ((triple2) -> rule1)) -> rule5))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Dave is white.
("Dave" "is" "white" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
((triple1) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((triple2) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple3) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((triple1 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((triple1 ((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2