Anne is big. Anne is blue. Anne is red. Anne is rough. Anne is not smart. Bob is not cold. Bob is not red. Bob is rough. Bob is not smart. Charlie is big. Charlie is not cold. Charlie is smart. Harry is big. Harry is red. Harry is not smart. All smart things are red. If something is blue and not kind then it is red. If something is big and not red then it is cold.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is not smart.
("Anne" "is" "smart" "-")
Bob is not cold.
("Bob" "is" "cold" "-")
Bob is not red.
("Bob" "is" "red" "-")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is not smart.
("Bob" "is" "smart" "-")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is smart.
("Charlie" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
All smart things are red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
If something is blue and not kind then it is red.
((("something" "is" "blue" "+") ("something" "is" "kind" "~")) -> ("something" "is" "red" "+"))
If something is big and not red then it is cold.
((("something" "is" "big" "+") ("something" "is" "red" "~")) -> ("something" "is" "cold" "+"))
Anne is not smart.
True
1
proof
[(triple5)]
("Anne" "is" "smart" "-")
triple5
Anne is not red.
False
1
inv-proof
[(triple3)]
("Anne" "is" "red" "-")
triple3
Charlie is red.
True
2
proof
[(((triple12) -> rule1))]
("Charlie" "is" "red" "+")
((triple12) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is not red.
False
2
inv-proof
[(((triple12) -> rule1))]
("Charlie" "is" "red" "-")
((triple12) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Anne is not cold.
Unknown
inv-rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "cold" "-")
Harry is cold.
Unknown
rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "cold" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is not smart.[(triple5)] Anne is red.[(triple3)] Anne is rough.[(triple4)] Bob is not cold.[(triple6)] Bob is not red.[(triple7)] Bob is not smart.[(triple9)] Bob is rough.[(triple8)] Charlie is big.[(triple10)] Charlie is not cold.[(triple11)] Charlie is smart.[(triple12)] Harry is big.[(triple13)] Harry is not smart.[(triple15)] Harry is red.[(triple14)] @1: Charlie is red.[(((triple12) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is not smart.
("Anne" "is" "smart" "-")
triple5
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Bob is not cold.
("Bob" "is" "cold" "-")
triple6
Bob is not red.
("Bob" "is" "red" "-")
triple7
Bob is not smart.
("Bob" "is" "smart" "-")
triple9
Bob is rough.
("Bob" "is" "rough" "+")
triple8
Charlie is big.
("Charlie" "is" "big" "+")
triple10
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple11
Charlie is smart.
("Charlie" "is" "smart" "+")
triple12
Harry is big.
("Harry" "is" "big" "+")
triple13
Harry is not smart.
("Harry" "is" "smart" "-")
triple15
Harry is red.
("Harry" "is" "red" "+")
triple14
Charlie is red.
("Charlie" "is" "red" "+")
((triple12) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1