Charlie is furry. Gary is nice. Gary is round. If something is nice and blue then it is big. Furry things are round. All furry things are blue. Round things are furry. Big things are red. All nice things are round. If Charlie is red then Charlie is big. If Gary is red and Gary is big then Gary is blue.
Charlie is furry.
("Charlie" "is" "furry" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is round.
("Gary" "is" "round" "+")
If something is nice and blue then it is big.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
Furry things are round.
((("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
All furry things are blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
Round things are furry.
((("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
Big things are red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
All nice things are round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
If Charlie is red then Charlie is big.
((("Charlie" "is" "red" "+")) -> ("Charlie" "is" "big" "+"))
If Gary is red and Gary is big then Gary is blue.
((("Gary" "is" "red" "+") ("Gary" "is" "big" "+")) -> ("Gary" "is" "blue" "+"))
Charlie is furry.
True
1
proof
[(triple1)]
("Charlie" "is" "furry" "+")
triple1
Gary is not nice.
False
1
inv-proof
[(triple2)]
("Gary" "is" "nice" "-")
triple2
Charlie is blue.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "blue" "+")
((triple1) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not blue.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "blue" "-")
((triple1) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Gary is blue.
True
3
proof
[(((((triple3) -> rule4)) -> rule3) OR ((((((triple2) -> rule6)) -> rule4)) -> rule3))]
("Gary" "is" "blue" "+")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is not blue.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule3) OR ((((((triple2) -> rule6)) -> rule4)) -> rule3))]
("Gary" "is" "blue" "-")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is big.
True
5
proof
[(((triple2 ((((triple3) -> rule4)) -> rule3)) -> rule1) OR ((triple2 ((((((triple2) -> rule6)) -> rule4)) -> rule3)) -> rule1))]
("Gary" "is" "big" "+")
((triple2 ((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((triple2 ((((((triple2) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is not big.
False
5
inv-proof
[(((triple2 ((((triple3) -> rule4)) -> rule3)) -> rule1) OR ((triple2 ((((((triple2) -> rule6)) -> rule4)) -> rule3)) -> rule1))]
("Gary" "is" "big" "-")
((triple2 ((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((triple2 ((((((triple2) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Charlie is not big.
Unknown
inv-rconc
[@3: Charlie is big.[CWA. Example of deepest failure = (rule7 <- rule5 <- rule1 <- FAIL)]]
("Charlie" "is" "big" "-")
Charlie is red.
Unknown
rconc
[@2: Charlie is red.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Charlie" "is" "red" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Charlie is furry.[(triple1)] Gary is nice.[(triple2)] Gary is round.[(triple3 OR ((triple2) -> rule6))] @1: Charlie is blue.[(((triple1) -> rule3))] Charlie is round.[(((triple1) -> rule2))] Gary is furry.[(((triple3) -> rule4) OR ((((triple2) -> rule6)) -> rule4))] @2: Gary is blue.[(((((triple3) -> rule4)) -> rule3) OR ((((((triple2) -> rule6)) -> rule4)) -> rule3))] @3: Gary is big.[(((triple2 ((((triple3) -> rule4)) -> rule3)) -> rule1) OR ((triple2 ((((((triple2) -> rule6)) -> rule4)) -> rule3)) -> rule1))] @4: Gary is red.[(((((triple2 ((((triple3) -> rule4)) -> rule3)) -> rule1)) -> rule5) OR ((((triple2 ((((((triple2) -> rule6)) -> rule4)) -> rule3)) -> rule1)) -> rule5))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Gary is nice.
("Gary" "is" "nice" "+")
triple2
Gary is round.
("Gary" "is" "round" "+")
triple3
((triple2) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple1) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple1) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple3) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
((triple2 ((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((triple2 ((((((triple2) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is red.
("Gary" "is" "red" "+")
((((triple2 ((((triple3) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
int4
((((triple2 ((((((triple2) -> (rule6 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
int4
Gary is round.
("Gary" "is" "round" "+")
int5