Anne is white. Bob is rough. Harry is blue. If Harry is big and Harry is nice then Harry is rough. All big things are red. Rough things are big. All blue things are big. Smart, rough things are blue. If something is big and nice then it is smart.
Anne is white.
("Anne" "is" "white" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Harry is blue.
("Harry" "is" "blue" "+")
If Harry is big and Harry is nice then Harry is rough.
((("Harry" "is" "big" "+") ("Harry" "is" "nice" "+")) -> ("Harry" "is" "rough" "+"))
All big things are red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
Rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
All blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
Smart, rough things are blue.
((("something" "is" "smart" "+") ("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
If something is big and nice then it is smart.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
Anne is white.
True
1
proof
[(triple1)]
("Anne" "is" "white" "+")
triple1
Anne is not white.
False
1
inv-proof
[(triple1)]
("Anne" "is" "white" "-")
triple1
Bob is big.
True
2
proof
[(((triple2) -> rule3))]
("Bob" "is" "big" "+")
((triple2) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is not big.
False
2
inv-proof
[(((triple2) -> rule3))]
("Bob" "is" "big" "-")
((triple2) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "smart" "-")
Bob is blue.
Unknown
rconc
[@2: Bob is blue.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Bob" "is" "blue" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is white.[(triple1)] Bob is rough.[(triple2)] Harry is blue.[(triple3)] @1: Bob is big.[(((triple2) -> rule3))] Harry is big.[(((triple3) -> rule4))] @2: Bob is red.[(((((triple2) -> rule3)) -> rule2))] Harry is red.[(((((triple3) -> rule4)) -> rule2))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Harry is blue.
("Harry" "is" "blue" "+")
triple3
Bob is big.
("Bob" "is" "big" "+")
((triple2) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple3) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2