Anne is blue. Anne is nice. Charlie is big. Charlie is furry. Charlie is kind. Charlie is nice. Charlie is round. Erin is blue. Erin is furry. Erin is nice. Erin is round. Erin is white. All white, big people are blue. If someone is nice then they are big. If Erin is white and Erin is nice then Erin is round. If Anne is white and Anne is big then Anne is round. All nice, white people are round. If someone is white then they are nice. Nice people are furry. If someone is round and blue then they are nice.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
All white, big people are blue.
((("someone" "is" "white" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
If someone is nice then they are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If Erin is white and Erin is nice then Erin is round.
((("Erin" "is" "white" "+") ("Erin" "is" "nice" "+")) -> ("Erin" "is" "round" "+"))
If Anne is white and Anne is big then Anne is round.
((("Anne" "is" "white" "+") ("Anne" "is" "big" "+")) -> ("Anne" "is" "round" "+"))
All nice, white people are round.
((("someone" "is" "nice" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
If someone is white then they are nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
Nice people are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
If someone is round and blue then they are nice.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
Erin is white.
True
1
proof
[(triple12)]
("Erin" "is" "white" "+")
triple12
Erin is not white.
False
1
inv-proof
[(triple12)]
("Erin" "is" "white" "-")
triple12
Erin is big.
True
2
proof
[(((triple10) -> rule2) OR ((((triple12) -> rule6)) -> rule2) OR ((((triple11 triple8) -> rule8)) -> rule2))]
("Erin" "is" "big" "+")
((triple10) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple12) -> (rule6 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple11 triple8) -> (rule8 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Anne is not furry.
False
2
inv-proof
[(((triple2) -> rule7))]
("Anne" "is" "furry" "-")
((triple2) -> (rule7 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not round.
Unknown
inv-rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "round" "-")
Charlie is blue.
Unknown
rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "blue" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
@0: Anne is blue.[(triple1)] Anne is nice.[(triple2)] Charlie is big.[(triple3 OR ((triple6) -> rule2))] Charlie is furry.[(triple4 OR ((triple6) -> rule7))] Charlie is kind.[(triple5)] Charlie is nice.[(triple6)] Charlie is round.[(triple7)] Erin is blue.[(triple8 OR ((triple12 ((triple10) -> rule2)) -> rule1) OR ((triple12 ((((triple12) -> rule6)) -> rule2)) -> rule1))] Erin is furry.[(triple9 OR ((triple10) -> rule7) OR ((((triple12) -> rule6)) -> rule7) OR ((((triple11 triple8) -> rule8)) -> rule7))] Erin is nice.[(triple10 OR ((triple12) -> rule6) OR ((triple11 triple8) -> rule8))] Erin is round.[(triple11 OR ((triple10 triple12) -> rule5) OR ((triple12 triple10) -> rule3) OR ((triple12 ((triple12) -> rule6)) -> rule3) OR ((((triple12) -> rule6) triple12) -> rule5))] Erin is white.[(triple12)] @1: Anne is big.[(((triple2) -> rule2))] Anne is furry.[(((triple2) -> rule7))] Erin is big.[(((triple10) -> rule2) OR ((((triple12) -> rule6)) -> rule2) OR ((((triple11 triple8) -> rule8)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
((triple6) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple4
((triple6) -> (rule7 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple5
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
Charlie is round.
("Charlie" "is" "round" "+")
triple7
Erin is blue.
("Erin" "is" "blue" "+")
triple8
((triple12 ((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((triple12 ((((triple12) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
triple9
((triple10) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((triple12) -> (rule6 % int2))) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple11 triple8) -> (rule8 % int2))) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
triple10
((triple12) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple11 triple8) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple11
((triple10 triple12) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple12 triple10) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple12 ((triple12) -> (rule6 % int2))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple12) -> (rule6 % int2)) triple12) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
triple12
Anne is big.
("Anne" "is" "big" "+")
((triple2) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((triple2) -> (rule7 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple10) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple12) -> (rule6 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple11 triple8) -> (rule8 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2