Anne is big. Anne is blue. Anne is not cold. Anne is red. Bob is not blue. Bob is round. Bob is white. Charlie is big. Charlie is not red. Gary is blue. Gary is round. Gary is white. If someone is blue and not cold then they are rough. Rough people are round. If someone is round then they are white.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is not cold.
("Anne" "is" "cold" "-")
Anne is red.
("Anne" "is" "red" "+")
Bob is not blue.
("Bob" "is" "blue" "-")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is not red.
("Charlie" "is" "red" "-")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
If someone is blue and not cold then they are rough.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "rough" "+"))
Rough people are round.
((("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
If someone is round then they are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
Bob is not blue.
True
1
proof
[(triple5)]
("Bob" "is" "blue" "-")
triple5
Charlie is red.
False
1
inv-proof
[(triple9)]
("Charlie" "is" "red" "+")
triple9
Anne is rough.
True
3
proof
[(((triple2 triple3) -> rule1))]
("Anne" "is" "rough" "+")
((triple2 triple3) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not rough.
False
3
inv-proof
[(((triple2 triple3) -> rule1))]
("Anne" "is" "rough" "-")
((triple2 triple3) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
True
4
proof
[(((((triple2 triple3) -> rule1)) -> rule2))]
("Anne" "is" "round" "+")
((((triple2 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not round.
False
4
inv-proof
[(((((triple2 triple3) -> rule1)) -> rule2))]
("Anne" "is" "round" "-")
((((triple2 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is white.
True
5
proof
[(((((((triple2 triple3) -> rule1)) -> rule2)) -> rule3))]
("Anne" "is" "white" "+")
((((((triple2 triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is not white.
False
5
inv-proof
[(((((((triple2 triple3) -> rule1)) -> rule2)) -> rule3))]
("Anne" "is" "white" "-")
((((((triple2 triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Charlie is not white.
Unknown
inv-rconc
[@3: Charlie is white.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule1 <- FAIL)]]
("Charlie" "is" "white" "-")
Gary is rough.
Unknown
rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "rough" "+")
Charlie is not round.
Unknown
inv-rconc
[@2: Charlie is round.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Charlie" "is" "round" "-")
Bob is rough.
Unknown
rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "rough" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is not cold.[(triple3)] Anne is red.[(triple4)] Bob is not blue.[(triple5)] Bob is round.[(triple6)] Bob is white.[(triple7 OR ((triple6) -> rule3))] Charlie is big.[(triple8)] Charlie is not red.[(triple9)] Gary is blue.[(triple10)] Gary is round.[(triple11)] Gary is white.[(triple12 OR ((triple11) -> rule3))] @1: Anne is rough.[(((triple2 triple3) -> rule1))] @2: Anne is round.[(((((triple2 triple3) -> rule1)) -> rule2))] @3: Anne is white.[(((((((triple2 triple3) -> rule1)) -> rule2)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is not cold.
("Anne" "is" "cold" "-")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
Bob is not blue.
("Bob" "is" "blue" "-")
triple5
Bob is round.
("Bob" "is" "round" "+")
triple6
Bob is white.
("Bob" "is" "white" "+")
triple7
((triple6) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
triple8
Charlie is not red.
("Charlie" "is" "red" "-")
triple9
Gary is blue.
("Gary" "is" "blue" "+")
triple10
Gary is round.
("Gary" "is" "round" "+")
triple11
Gary is white.
("Gary" "is" "white" "+")
triple12
((triple11) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((triple2 triple3) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((((triple2 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
((((((triple2 triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3