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