Anne is big. Bob is big. Bob is blue. Bob is cold. Bob is green. Bob is quiet. Bob is white. Bob is young. Charlie is big. Charlie is green. Charlie is quiet. Charlie is white. Charlie is young. Erin is blue. Erin is cold. Erin is white. All quiet, big people are green. All big people are quiet. If someone is quiet and green then they are cold.
Anne is big.
("Anne" "is" "big" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is white.
("Erin" "is" "white" "+")
All quiet, big people are green.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
All big people are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
If someone is quiet and green then they are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
Erin is white.
True
1
proof
[(triple16)]
("Erin" "is" "white" "+")
triple16
Erin is not white.
False
1
inv-proof
[(triple16)]
("Erin" "is" "white" "-")
triple16
Charlie is cold.
True
3
proof
[(((triple11 triple10) -> rule3) OR ((triple11 ((triple11 triple9) -> rule1)) -> rule3) OR ((((triple9) -> rule2) triple10) -> rule3) OR ((((triple9) -> rule2) ((triple11 triple9) -> rule1)) -> rule3) OR ((triple11 ((((triple9) -> rule2) triple9) -> rule1)) -> rule3) OR ((((triple9) -> rule2) ((((triple9) -> rule2) triple9) -> rule1)) -> rule3))]
("Charlie" "is" "cold" "+")
((triple11 triple10) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple11 ((triple11 triple9) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((triple9) -> (rule2 % int2)) triple10) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple9) -> (rule2 % int3)) ((triple11 triple9) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((triple11 ((((triple9) -> (rule2 % int3)) triple9) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((triple9) -> (rule2 % int3)) ((((triple9) -> (rule2 % int3)) triple9) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Anne is not quiet.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "quiet" "-")
((triple1) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is green.
True
4
proof
[(((((triple1) -> rule2) triple1) -> rule1))]
("Anne" "is" "green" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not green.
False
4
inv-proof
[(((((triple1) -> rule2) triple1) -> rule1))]
("Anne" "is" "green" "-")
((((triple1) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is cold.
True
7
proof
[(((((triple1) -> rule2) ((((triple1) -> rule2) triple1) -> rule1)) -> rule3))]
("Anne" "is" "cold" "+")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3)) triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is not cold.
False
7
inv-proof
[(((((triple1) -> rule2) ((((triple1) -> rule2) triple1) -> rule1)) -> rule3))]
("Anne" "is" "cold" "-")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3)) triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "quiet" "-")
Erin is green.
Unknown
rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "green" "+")
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
@0: Anne is big.[(triple1)] Bob is big.[(triple2)] Bob is blue.[(triple3)] Bob is cold.[(triple4 OR ((triple6 triple5) -> rule3) OR ((triple6 ((triple6 triple2) -> rule1)) -> rule3) OR ((((triple2) -> rule2) triple5) -> rule3) OR ((((triple2) -> rule2) ((triple6 triple2) -> rule1)) -> rule3) OR ((triple6 ((((triple2) -> rule2) triple2) -> rule1)) -> rule3) OR ((((triple2) -> rule2) ((((triple2) -> rule2) triple2) -> rule1)) -> rule3))] Bob is green.[(triple5 OR ((triple6 triple2) -> rule1) OR ((((triple2) -> rule2) triple2) -> rule1))] Bob is quiet.[(triple6 OR ((triple2) -> rule2))] Bob is white.[(triple7)] Bob is young.[(triple8)] Charlie is big.[(triple9)] Charlie is green.[(triple10 OR ((triple11 triple9) -> rule1) OR ((((triple9) -> rule2) triple9) -> rule1))] Charlie is quiet.[(triple11 OR ((triple9) -> rule2))] Charlie is white.[(triple12)] Charlie is young.[(triple13)] Erin is blue.[(triple14)] Erin is cold.[(triple15)] Erin is white.[(triple16)] @1: Anne is quiet.[(((triple1) -> rule2))] Charlie is cold.[(((triple11 triple10) -> rule3) OR ((triple11 ((triple11 triple9) -> rule1)) -> rule3) OR ((((triple9) -> rule2) triple10) -> rule3) OR ((((triple9) -> rule2) ((triple11 triple9) -> rule1)) -> rule3) OR ((triple11 ((((triple9) -> rule2) triple9) -> rule1)) -> rule3) OR ((((triple9) -> rule2) ((((triple9) -> rule2) triple9) -> rule1)) -> rule3))] @2: Anne is green.[(((((triple1) -> rule2) triple1) -> rule1))] @3: Anne is cold.[(((((triple1) -> rule2) ((((triple1) -> rule2) triple1) -> rule1)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Bob is big.
("Bob" "is" "big" "+")
triple2
Bob is blue.
("Bob" "is" "blue" "+")
triple3
Bob is cold.
("Bob" "is" "cold" "+")
triple4
((triple6 triple5) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple6 ((triple6 triple2) -> (rule1 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple2) -> (rule2 % int2)) triple5) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((triple2) -> (rule2 % int3)) ((triple6 triple2) -> (rule1 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
((triple6 ((((triple2) -> (rule2 % int3)) triple2) -> (rule1 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
((((triple2) -> (rule2 % int3)) ((((triple2) -> (rule2 % int3)) triple2) -> (rule1 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
triple5
((triple6 triple2) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple2) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple6
((triple2) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple7
Bob is young.
("Bob" "is" "young" "+")
triple8
Charlie is big.
("Charlie" "is" "big" "+")
triple9
Charlie is green.
("Charlie" "is" "green" "+")
triple10
((triple11 triple9) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((((triple9) -> (rule2 % int2)) triple9) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple11
((triple9) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple12
Charlie is young.
("Charlie" "is" "young" "+")
triple13
Erin is blue.
("Erin" "is" "blue" "+")
triple14
Erin is cold.
("Erin" "is" "cold" "+")
triple15
Erin is white.
("Erin" "is" "white" "+")
triple16
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple11 triple10) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple11 ((triple11 triple9) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((triple9) -> (rule2 % int2)) triple10) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple9) -> (rule2 % int3)) ((triple11 triple9) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((triple11 ((((triple9) -> (rule2 % int3)) triple9) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((triple9) -> (rule2 % int3)) ((((triple9) -> (rule2 % int3)) triple9) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3)) triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3