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