Anne is big. Anne is cold. Anne is green. Anne is not kind. Anne is red. Charlie is red. Gary is blue. Gary is red. Harry is green. Harry is not red. Green, red people are round. If someone is cold and not green then they are round. If someone is green then they are round. All blue, round people are cold. Round people are blue. If Charlie is round and Charlie is not cold then Charlie is kind.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is not kind.
("Anne" "is" "kind" "-")
Anne is red.
("Anne" "is" "red" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is red.
("Gary" "is" "red" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is not red.
("Harry" "is" "red" "-")
Green, red people are round.
((("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If someone is cold and not green then they are round.
((("someone" "is" "cold" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "round" "+"))
If someone is green then they are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
All blue, round people are cold.
((("someone" "is" "blue" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
Round people are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If Charlie is round and Charlie is not cold then Charlie is kind.
((("Charlie" "is" "round" "+") ("Charlie" "is" "cold" "~")) -> ("Charlie" "is" "kind" "+"))
Harry is green.
True
1
proof
[(triple9)]
("Harry" "is" "green" "+")
triple9
Harry is not green.
False
1
inv-proof
[(triple9)]
("Harry" "is" "green" "-")
triple9
Anne is round.
True
2
proof
[(((triple3) -> rule3) OR ((triple3 triple5) -> rule1))]
("Anne" "is" "round" "+")
((triple3) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((triple3 triple5) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not round.
False
2
inv-proof
[(((triple3) -> rule3) OR ((triple3 triple5) -> rule1))]
("Anne" "is" "round" "-")
((triple3) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((triple3 triple5) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Harry is blue.
True
3
proof
[(((((triple9) -> rule3)) -> rule5))]
("Harry" "is" "blue" "+")
((((triple9) -> (rule3 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not blue.
False
3
inv-proof
[(((((triple9) -> rule3)) -> rule5))]
("Harry" "is" "blue" "-")
((((triple9) -> (rule3 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Charlie is not kind.
Unknown
inv-rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "kind" "-")
Gary is cold.
Unknown
rconc
[@2: Gary is cold.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Gary" "is" "cold" "+")
Charlie is not cold.
Unknown
inv-rconc
[@2: Charlie is cold.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Charlie" "is" "cold" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Anne is big.[(triple1)] Anne is cold.[(triple2 OR ((((((triple3) -> rule3)) -> rule5) ((triple3) -> rule3)) -> rule4) OR ((((((triple3) -> rule3)) -> rule5) ((triple3 triple5) -> rule1)) -> rule4) OR ((((((triple3 triple5) -> rule1)) -> rule5) ((triple3) -> rule3)) -> rule4) OR ((((((triple3 triple5) -> rule1)) -> rule5) ((triple3 triple5) -> rule1)) -> rule4))] Anne is green.[(triple3)] Anne is not kind.[(triple4)] Anne is red.[(triple5)] Charlie is red.[(triple6)] Gary is blue.[(triple7)] Gary is red.[(triple8)] Harry is green.[(triple9)] Harry is not red.[(triple10)] @1: Anne is round.[(((triple3) -> rule3) OR ((triple3 triple5) -> rule1))] Harry is round.[(((triple9) -> rule3))] @2: Anne is blue.[(((((triple3) -> rule3)) -> rule5) OR ((((triple3 triple5) -> rule1)) -> rule5))] Harry is blue.[(((((triple9) -> rule3)) -> rule5))] @3: Harry is cold.[(((((((triple9) -> rule3)) -> rule5) ((triple9) -> rule3)) -> rule4))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2)) ((triple3) -> (rule3 % int3))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2)) ((triple3 triple5) -> (rule1 % int3))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
((((((triple3 triple5) -> (rule1 % int3))) -> (rule5 % int2)) ((triple3) -> (rule3 % int3))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
((((((triple3 triple5) -> (rule1 % int3))) -> (rule5 % int2)) ((triple3 triple5) -> (rule1 % int3))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is not kind.
("Anne" "is" "kind" "-")
triple4
Anne is red.
("Anne" "is" "red" "+")
triple5
Charlie is red.
("Charlie" "is" "red" "+")
triple6
Gary is blue.
("Gary" "is" "blue" "+")
triple7
Gary is red.
("Gary" "is" "red" "+")
triple8
Harry is green.
("Harry" "is" "green" "+")
triple9
Harry is not red.
("Harry" "is" "red" "-")
triple10
Anne is round.
("Anne" "is" "round" "+")
((triple3) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((triple3 triple5) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple9) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((triple3 triple5) -> (rule1 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((((triple9) -> (rule3 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((((((triple9) -> (rule3 % int3))) -> (rule5 % int2)) ((triple9) -> (rule3 % int3))) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3