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