Anne is cold. Anne is green. Anne is nice. Anne is smart. Bob is blue. Bob is green. Bob is nice. Bob is smart. Bob is white. Charlie is blue. If something is round then it is blue. If Anne is cold and Anne is white then Anne is round. All green, nice things are white.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
If something is round then it is blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
If Anne is cold and Anne is white then Anne is round.
((("Anne" "is" "cold" "+") ("Anne" "is" "white" "+")) -> ("Anne" "is" "round" "+"))
All green, nice things are white.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
Bob is nice.
True
1
proof
[(triple7)]
("Bob" "is" "nice" "+")
triple7
Anne is not cold.
False
1
inv-proof
[(triple1)]
("Anne" "is" "cold" "-")
triple1
Anne is white.
True
3
proof
[(((triple2 triple3) -> rule3))]
("Anne" "is" "white" "+")
((triple2 triple3) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not white.
False
3
inv-proof
[(((triple2 triple3) -> rule3))]
("Anne" "is" "white" "-")
((triple2 triple3) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is round.
True
5
proof
[(((triple1 ((triple2 triple3) -> rule3)) -> rule2))]
("Anne" "is" "round" "+")
((triple1 ((triple2 triple3) -> (rule3 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is not round.
False
5
inv-proof
[(((triple1 ((triple2 triple3) -> rule3)) -> rule2))]
("Anne" "is" "round" "-")
((triple1 ((triple2 triple3) -> (rule3 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
True
6
proof
[(((((triple1 ((triple2 triple3) -> rule3)) -> rule2)) -> rule1))]
("Anne" "is" "blue" "+")
((((triple1 ((triple2 triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is not blue.
False
6
inv-proof
[(((((triple1 ((triple2 triple3) -> rule3)) -> rule2)) -> rule1))]
("Anne" "is" "blue" "-")
((((triple1 ((triple2 triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "white" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Anne is cold.[(triple1)] Anne is green.[(triple2)] Anne is nice.[(triple3)] Anne is smart.[(triple4)] Bob is blue.[(triple5)] Bob is green.[(triple6)] Bob is nice.[(triple7)] Bob is smart.[(triple8)] Bob is white.[(triple9 OR ((triple6 triple7) -> rule3))] Charlie is blue.[(triple10)] @1: Anne is white.[(((triple2 triple3) -> rule3))] @2: Anne is round.[(((triple1 ((triple2 triple3) -> rule3)) -> rule2))] @3: Anne is blue.[(((((triple1 ((triple2 triple3) -> rule3)) -> rule2)) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Bob is blue.
("Bob" "is" "blue" "+")
triple5
Bob is green.
("Bob" "is" "green" "+")
triple6
Bob is nice.
("Bob" "is" "nice" "+")
triple7
Bob is smart.
("Bob" "is" "smart" "+")
triple8
Bob is white.
("Bob" "is" "white" "+")
triple9
((triple6 triple7) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple10
Anne is white.
("Anne" "is" "white" "+")
((triple2 triple3) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((triple1 ((triple2 triple3) -> (rule3 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1 ((triple2 triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3