Anne is red. Bob is red. Bob is rough. Charlie is green. Harry is cold. Harry is green. Harry is round. If Harry is cold and Harry is round then Harry is smart. Rough, red things are cold. If something is round then it is big. All red things are big. All round things are green. If something is cold and red then it is rough. If something is smart and green then it is big. If something is smart then it is big.
Anne is red.
("Anne" "is" "red" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is round.
("Harry" "is" "round" "+")
If Harry is cold and Harry is round then Harry is smart.
((("Harry" "is" "cold" "+") ("Harry" "is" "round" "+")) -> ("Harry" "is" "smart" "+"))
Rough, red things are cold.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If something is round then it is big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
All red things are big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
All round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
If something is cold and red then it is rough.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If something is smart and green then it is big.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If something is smart then it is big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
Harry is cold.
True
1
proof
[(triple5)]
("Harry" "is" "cold" "+")
triple5
Harry is not cold.
False
1
inv-proof
[(triple5)]
("Harry" "is" "cold" "-")
triple5
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "green" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Anne is red.[(triple1)] Bob is red.[(triple2)] Bob is rough.[(triple3)] Charlie is green.[(triple4)] Harry is cold.[(triple5)] Harry is green.[(triple6 OR ((triple7) -> rule5))] Harry is round.[(triple7)] @1: Anne is big.[(((triple1) -> rule4))] Bob is big.[(((triple2) -> rule4))] Bob is cold.[(((triple3 triple2) -> rule2))] Harry is big.[(((triple7) -> rule3) OR ((((triple5 triple7) -> rule1)) -> rule8) OR ((((triple5 triple7) -> rule1) triple6) -> rule7) OR ((((triple5 triple7) -> rule1) ((triple7) -> rule5)) -> rule7))] Harry is smart.[(((triple5 triple7) -> rule1))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
triple4
Harry is cold.
("Harry" "is" "cold" "+")
triple5
Harry is green.
("Harry" "is" "green" "+")
triple6
((triple7) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple7
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((triple2) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((triple3 triple2) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple7) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((((triple5 triple7) -> (rule1 % int2))) -> (rule8 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((triple5 triple7) -> (rule1 % int2)) triple6) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((triple5 triple7) -> (rule1 % int3)) ((triple7) -> (rule5 % int2))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
((triple5 triple7) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1