Anne is blue. Anne is kind. Anne is nice. Anne is red. Anne is round. Bob is big. Bob is kind. Bob is round. Charlie is big. Charlie is blue. Charlie is kind. Charlie is rough. Erin is kind. Erin is nice. Erin is rough. Erin is round. If something is round and blue then it is kind. Round things are blue. If Bob is red then Bob is rough. All blue things are big. If something is red then it is kind. If Bob is blue then Bob is red. If Erin is round then Erin is big. If Erin is red then Erin is blue.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
If something is round and blue then it is kind.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
Round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
If Bob is red then Bob is rough.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "rough" "+"))
All blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If something is red then it is kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If Bob is blue then Bob is red.
((("Bob" "is" "blue" "+")) -> ("Bob" "is" "red" "+"))
If Erin is round then Erin is big.
((("Erin" "is" "round" "+")) -> ("Erin" "is" "big" "+"))
If Erin is red then Erin is blue.
((("Erin" "is" "red" "+")) -> ("Erin" "is" "blue" "+"))
Anne is kind.
True
1
proof
[(triple2 OR ((triple4) -> rule5) OR ((triple5 triple1) -> rule1) OR ((triple5 ((triple5) -> rule2)) -> rule1))]
("Anne" "is" "kind" "+")
triple2
((triple4) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple5 triple1) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple5 ((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Erin is not rough.
False
1
inv-proof
[(triple15)]
("Erin" "is" "rough" "-")
triple15
Anne is big.
True
2
proof
[(((triple1) -> rule4) OR ((((triple5) -> rule2)) -> rule4))]
("Anne" "is" "big" "+")
((triple1) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Erin is not big.
False
2
inv-proof
[(((triple16) -> rule7) OR ((((triple16) -> rule2)) -> rule4))]
("Erin" "is" "big" "-")
((triple16) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple16) -> (rule2 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Bob is red.
True
3
proof
[(((((triple8) -> rule2)) -> rule6))]
("Bob" "is" "red" "+")
((((triple8) -> (rule2 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is not red.
False
3
inv-proof
[(((((triple8) -> rule2)) -> rule6))]
("Bob" "is" "red" "-")
((((triple8) -> (rule2 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
True
4
proof
[(((((((triple8) -> rule2)) -> rule6)) -> rule3))]
("Bob" "is" "rough" "+")
((((((triple8) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is not rough.
False
4
inv-proof
[(((((((triple8) -> rule2)) -> rule6)) -> rule3))]
("Bob" "is" "rough" "-")
((((((triple8) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Anne is blue.[(triple1 OR ((triple5) -> rule2))] Anne is kind.[(triple2 OR ((triple4) -> rule5) OR ((triple5 triple1) -> rule1) OR ((triple5 ((triple5) -> rule2)) -> rule1))] Anne is nice.[(triple3)] Anne is red.[(triple4)] Anne is round.[(triple5)] Bob is big.[(triple6 OR ((((triple8) -> rule2)) -> rule4))] Bob is kind.[(triple7 OR ((triple8 ((triple8) -> rule2)) -> rule1) OR ((((((triple8) -> rule2)) -> rule6)) -> rule5))] Bob is round.[(triple8)] Charlie is big.[(triple9 OR ((triple10) -> rule4))] Charlie is blue.[(triple10)] Charlie is kind.[(triple11)] Charlie is rough.[(triple12)] Erin is kind.[(triple13 OR ((triple16 ((triple16) -> rule2)) -> rule1))] Erin is nice.[(triple14)] Erin is rough.[(triple15)] Erin is round.[(triple16)] @1: Anne is big.[(((triple1) -> rule4) OR ((((triple5) -> rule2)) -> rule4))] Bob is blue.[(((triple8) -> rule2))] Erin is big.[(((triple16) -> rule7) OR ((((triple16) -> rule2)) -> rule4))] Erin is blue.[(((triple16) -> rule2))] @2: Bob is red.[(((((triple8) -> rule2)) -> rule6))] @3: Bob is rough.[(((((((triple8) -> rule2)) -> rule6)) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((triple5) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
((triple4) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple5 triple1) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple5 ((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
triple5
Bob is big.
("Bob" "is" "big" "+")
triple6
((((triple8) -> (rule2 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
triple7
((triple8 ((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((((triple8) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
triple8
Charlie is big.
("Charlie" "is" "big" "+")
triple9
((triple10) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple10
Charlie is kind.
("Charlie" "is" "kind" "+")
triple11
Charlie is rough.
("Charlie" "is" "rough" "+")
triple12
Erin is kind.
("Erin" "is" "kind" "+")
triple13
((triple16 ((triple16) -> (rule2 % int2))) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
triple14
Erin is rough.
("Erin" "is" "rough" "+")
triple15
Erin is round.
("Erin" "is" "round" "+")
triple16
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
((triple8) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple16) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple16) -> (rule2 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
((triple16) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((((triple8) -> (rule2 % int2))) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((((((triple8) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3