Anne is rough. Bob is white. Rough things are big. If Bob is quiet then Bob is rough. Green, white things are rough. If something is cold and rough then it is green. Big things are green. All cold things are white. If something is cold and nice then it is big. Cold things are big.
Anne is rough.
("Anne" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If Bob is quiet then Bob is rough.
((("Bob" "is" "quiet" "+")) -> ("Bob" "is" "rough" "+"))
Green, white things are rough.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
If something is cold and rough then it is green.
((("something" "is" "cold" "+") ("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
Big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
All cold things are white.
((("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
If something is cold and nice then it is big.
((("something" "is" "cold" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
Cold things are big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
Bob is white.
True
1
proof
[(triple2)]
("Bob" "is" "white" "+")
triple2
Anne is not rough.
False
1
inv-proof
[(triple1)]
("Anne" "is" "rough" "-")
triple1
Bob is not big.
Unknown
inv-rconc
[@4: Bob is big.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule5 <- rule7 <- FAIL)]]
("Bob" "is" "big" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Anne is rough.[(triple1)] Bob is white.[(triple2)] @1: Anne is big.[(((triple1) -> rule1))] @2: Anne is green.[(((((triple1) -> rule1)) -> rule5))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2