Anne is kind. Anne is smart. Bob is kind. Bob is quiet. Gary is big. Gary is blue. Gary is cold. Gary is green. Gary is smart. Harry is quiet. Green, quiet things are cold. All kind, blue things are cold. All smart things are blue. All blue things are big. All blue things are kind. If Anne is blue then Anne is smart.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Green, quiet things are cold.
((("something" "is" "green" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
All kind, blue things are cold.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
All smart things are blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
All blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
All blue things are kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If Anne is blue then Anne is smart.
((("Anne" "is" "blue" "+")) -> ("Anne" "is" "smart" "+"))
Bob is kind.
True
1
proof
[(triple3)]
("Bob" "is" "kind" "+")
triple3
Gary is not green.
False
1
inv-proof
[(triple8)]
("Gary" "is" "green" "-")
triple8
Harry is not kind.
Unknown
inv-rconc
[@2: Harry is kind.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Harry" "is" "kind" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is kind.[(triple1 OR ((((triple2) -> rule3)) -> rule5))] Anne is smart.[(triple2)] Bob is kind.[(triple3)] Bob is quiet.[(triple4)] Gary is big.[(triple5 OR ((triple6) -> rule4) OR ((((triple9) -> rule3)) -> rule4))] Gary is blue.[(triple6 OR ((triple9) -> rule3))] Gary is cold.[(triple7 OR ((((triple6) -> rule5) triple6) -> rule2) OR ((((triple6) -> rule5) ((triple9) -> rule3)) -> rule2) OR ((((((triple9) -> rule3)) -> rule5) triple6) -> rule2) OR ((((((triple9) -> rule3)) -> rule5) ((triple9) -> rule3)) -> rule2))] Gary is green.[(triple8)] Gary is smart.[(triple9)] Harry is quiet.[(triple10)] @1: Anne is blue.[(((triple2) -> rule3))] Gary is kind.[(((triple6) -> rule5) OR ((((triple9) -> rule3)) -> rule5))] @2: Anne is big.[(((((triple2) -> rule3)) -> rule4))] Anne is cold.[(((triple1 ((triple2) -> rule3)) -> rule2) OR ((((((triple2) -> rule3)) -> rule5) ((triple2) -> rule3)) -> rule2))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Gary is big.
("Gary" "is" "big" "+")
triple5
((triple6) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple9) -> (rule3 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
triple6
((triple9) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple7
((((triple6) -> (rule5 % int2)) triple6) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((((triple6) -> (rule5 % int3)) ((triple9) -> (rule3 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
((((((triple9) -> (rule3 % int3))) -> (rule5 % int2)) triple6) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
((((((triple9) -> (rule3 % int3))) -> (rule5 % int2)) ((triple9) -> (rule3 % int3))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
triple8
Gary is smart.
("Gary" "is" "smart" "+")
triple9
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Anne is blue.
("Anne" "is" "blue" "+")
((triple2) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple6) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((triple9) -> (rule3 % int2))) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((triple1 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2)) ((triple2) -> (rule3 % int3))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3