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