Charlie is blue. Charlie is furry. Charlie is young. Gary is blue. Gary is green. Gary is rough. Gary is young. If something is furry then it is young. If something is young then it is furry. All furry things are nice. All nice things are young. Blue things are green. If something is furry and blue then it is rough.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is young.
("Gary" "is" "young" "+")
If something is furry then it is young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
If something is young then it is furry.
((("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
All furry things are nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
All nice things are young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
Blue things are green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If something is furry and blue then it is rough.
((("something" "is" "furry" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
Charlie is furry.
True
1
proof
[(triple2 OR ((triple3) -> rule2))]
("Charlie" "is" "furry" "+")
triple2
((triple3) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Gary is not rough.
False
1
inv-proof
[(triple6 OR ((((triple7) -> rule2) triple4) -> rule6))]
("Gary" "is" "rough" "-")
triple6
((((triple7) -> (rule2 % int2)) triple4) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Charlie is rough.
True
3
proof
[(((triple2 triple1) -> rule6) OR ((((triple3) -> rule2) triple1) -> rule6))]
("Charlie" "is" "rough" "+")
((triple2 triple1) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple3) -> (rule2 % int2)) triple1) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is not nice.
False
2
inv-proof
[(((triple2) -> rule3) OR ((((triple3) -> rule2)) -> rule3))]
("Charlie" "is" "nice" "-")
((triple2) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Gary is nice.
True
3
proof
[(((((triple7) -> rule2)) -> rule3))]
("Gary" "is" "nice" "+")
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is not nice.
False
3
inv-proof
[(((((triple7) -> rule2)) -> rule3))]
("Gary" "is" "nice" "-")
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
@0: Charlie is blue.[(triple1)] Charlie is furry.[(triple2 OR ((triple3) -> rule2))] Charlie is young.[(triple3 OR ((triple2) -> rule1) OR ((((triple2) -> rule3)) -> rule4))] Gary is blue.[(triple4)] Gary is green.[(triple5 OR ((triple4) -> rule5))] Gary is rough.[(triple6 OR ((((triple7) -> rule2) triple4) -> rule6))] Gary is young.[(triple7)] @1: Charlie is green.[(((triple1) -> rule5))] Charlie is nice.[(((triple2) -> rule3) OR ((((triple3) -> rule2)) -> rule3))] Charlie is rough.[(((triple2 triple1) -> rule6) OR ((((triple3) -> rule2) triple1) -> rule6))] Gary is furry.[(((triple7) -> rule2))] @2: Gary is nice.[(((((triple7) -> rule2)) -> rule3))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
((triple3) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple3
((triple2) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
triple4
Gary is green.
("Gary" "is" "green" "+")
triple5
((triple4) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
triple6
((((triple7) -> (rule2 % int2)) triple4) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
((triple1) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple2) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple2 triple1) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple3) -> (rule2 % int2)) triple1) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((triple7) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2