Anne is blue. Anne is quiet. Charlie is blue. Charlie is rough. Charlie is young. Erin is cold. Erin is rough. Erin is young. Gary is blue. Gary is cold. Gary is quiet. All smart, quiet things are young. If something is young then it is smart. All quiet things are smart. If something is cold and quiet then it is not rough. If Erin is smart then Erin is blue. If Erin is not smart then Erin is blue. If something is nice then it is cold. If something is young then it is nice. If something is cold and blue then it is nice.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
All smart, quiet things are young.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
If something is young then it is smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
All quiet things are smart.
((("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
If something is cold and quiet then it is not rough.
((("something" "is" "cold" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "rough" "-"))
If Erin is smart then Erin is blue.
((("Erin" "is" "smart" "+")) -> ("Erin" "is" "blue" "+"))
If Erin is not smart then Erin is blue.
((("Erin" "is" "smart" "~")) -> ("Erin" "is" "blue" "+"))
If something is nice then it is cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If something is young then it is nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If something is cold and blue then it is nice.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Charlie is not blue.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "blue" "-")
triple3
Gary is smart.
True
2
proof
[(((triple11) -> rule3))]
("Gary" "is" "smart" "+")
((triple11) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Charlie is not smart.
False
2
inv-proof
[(((triple5) -> rule2))]
("Charlie" "is" "smart" "-")
((triple5) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Gary is young.
True
4
proof
[(((((triple11) -> rule3) triple11) -> rule1))]
("Gary" "is" "young" "+")
((((triple11) -> (rule3 % int2)) triple11) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not young.
False
4
inv-proof
[(((((triple11) -> rule3) triple11) -> rule1))]
("Gary" "is" "young" "-")
((((triple11) -> (rule3 % int2)) triple11) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Anne is nice.
True
5
proof
[(((((((triple2) -> rule3) triple2) -> rule1)) -> rule8))]
("Anne" "is" "nice" "+")
((((((triple2) -> (rule3 % int3)) triple2) -> (rule1 % int2))) -> (rule8 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is not nice.
False
5
inv-proof
[(((((((triple2) -> rule3) triple2) -> rule1)) -> rule8))]
("Anne" "is" "nice" "-")
((((((triple2) -> (rule3 % int3)) triple2) -> (rule1 % int2))) -> (rule8 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is cold.
True
6
proof
[(((((((((triple2) -> rule3) triple2) -> rule1)) -> rule8)) -> rule7))]
("Anne" "is" "cold" "+")
((((((((triple2) -> (rule3 % int4)) triple2) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is not cold.
False
6
inv-proof
[(((((((((triple2) -> rule3) triple2) -> rule1)) -> rule8)) -> rule7))]
("Anne" "is" "cold" "-")
((((((((triple2) -> (rule3 % int4)) triple2) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is not rough.
True
8
proof
[(((((((((((triple2) -> rule3) triple2) -> rule1)) -> rule8)) -> rule7) triple2) -> rule4))]
("Anne" "is" "rough" "-")
((((((((((triple2) -> (rule3 % int5)) triple2) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule7 % int2)) triple2) -> (rule4 % int1))
Anne is not rough.
("Anne" "is" "rough" "-")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is smart.
("Anne" "is" "smart" "+")
int5
Anne is rough.
False
8
inv-proof
[(((((((((((triple2) -> rule3) triple2) -> rule1)) -> rule8)) -> rule7) triple2) -> rule4))]
("Anne" "is" "rough" "+")
((((((((((triple2) -> (rule3 % int5)) triple2) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule7 % int2)) triple2) -> (rule4 % int1))
Anne is not rough.
("Anne" "is" "rough" "-")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is smart.
("Anne" "is" "smart" "+")
int5
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Anne is blue.[(triple1)] Anne is quiet.[(triple2)] Charlie is blue.[(triple3)] Charlie is rough.[(triple4)] Charlie is young.[(triple5)] Erin is cold.[(triple6 OR ((((triple8) -> rule8)) -> rule7))] Erin is rough.[(triple7)] Erin is young.[(triple8)] Gary is blue.[(triple9)] Gary is cold.[(triple10 OR ((((((((triple11) -> rule3) triple11) -> rule1)) -> rule8)) -> rule7))] Gary is quiet.[(triple11)] @1: Anne is smart.[(((triple2) -> rule3))] Charlie is nice.[(((triple5) -> rule8))] Charlie is smart.[(((triple5) -> rule2))] Erin is nice.[(((triple8) -> rule8) OR ((triple6 ((((triple8) -> rule2)) -> rule5)) -> rule9))] Erin is smart.[(((triple8) -> rule2))] Gary is nice.[(((triple10 triple9) -> rule9) OR ((((((triple11) -> rule3) triple11) -> rule1)) -> rule8))] Gary is not rough.[(((triple10 triple11) -> rule4) OR ((((((((((triple11) -> rule3) triple11) -> rule1)) -> rule8)) -> rule7) triple11) -> rule4))] Gary is smart.[(((triple11) -> rule3))] @2: Anne is young.[(((((triple2) -> rule3) triple2) -> rule1))] Charlie is cold.[(((((triple5) -> rule8)) -> rule7))] Erin is blue.[(((((triple8) -> rule2)) -> rule5))] Gary is young.[(((((triple11) -> rule3) triple11) -> rule1))] @3: Anne is nice.[(((((((triple2) -> rule3) triple2) -> rule1)) -> rule8))] @4: Anne is cold.[(((((((((triple2) -> rule3) triple2) -> rule1)) -> rule8)) -> rule7))] @5: Anne is not rough.[(((((((((((triple2) -> rule3) triple2) -> rule1)) -> rule8)) -> rule7) triple2) -> rule4))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Erin is cold.
("Erin" "is" "cold" "+")
triple6
((((triple8) -> (rule8 % int2))) -> (rule7 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
triple7
Erin is young.
("Erin" "is" "young" "+")
triple8
Gary is blue.
("Gary" "is" "blue" "+")
triple9
Gary is cold.
("Gary" "is" "cold" "+")
triple10
((((((((triple11) -> (rule3 % int4)) triple11) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
triple11
Anne is smart.
("Anne" "is" "smart" "+")
((triple2) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple5) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple5) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple8) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple6 ((((triple8) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule9 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
((triple8) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple10 triple9) -> (rule9 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((((triple11) -> (rule3 % int3)) triple11) -> (rule1 % int2))) -> (rule8 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not rough.
("Gary" "is" "rough" "-")
((triple10 triple11) -> (rule4 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
((((((((((triple11) -> (rule3 % int5)) triple11) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule7 % int2)) triple11) -> (rule4 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
int5
Gary is smart.
("Gary" "is" "smart" "+")
((triple11) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple2) -> (rule3 % int2)) triple2) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple5) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
((((triple8) -> (rule2 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((((triple11) -> (rule3 % int2)) triple11) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
((((((triple2) -> (rule3 % int3)) triple2) -> (rule1 % int2))) -> (rule8 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
((((((((triple2) -> (rule3 % int4)) triple2) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is not rough.
("Anne" "is" "rough" "-")
((((((((((triple2) -> (rule3 % int5)) triple2) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule7 % int2)) triple2) -> (rule4 % int1))
Anne is not rough.
("Anne" "is" "rough" "-")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is smart.
("Anne" "is" "smart" "+")
int5