Anne is green. Anne is quiet. Anne is rough. Anne is young. Bob is big. Bob is blue. Bob is kind. Bob is young. Gary is not big. Gary is blue. Gary is green. Gary is kind. Gary is quiet. Gary is rough. Gary is not young. If Gary is big and Gary is not green then Gary is quiet. Blue things are rough. If something is young and green then it is rough. Green, young things are rough. If Anne is rough then Anne is quiet. If something is young and not kind then it is blue. Green things are not big. If Anne is not blue and Anne is not green then Anne is big.
Anne is green.
("Anne" "is" "green" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is young.
("Bob" "is" "young" "+")
Gary is not big.
("Gary" "is" "big" "-")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is not young.
("Gary" "is" "young" "-")
If Gary is big and Gary is not green then Gary is quiet.
((("Gary" "is" "big" "+") ("Gary" "is" "green" "~")) -> ("Gary" "is" "quiet" "+"))
Blue things are rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If something is young and green then it is rough.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
Green, young things are rough.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If Anne is rough then Anne is quiet.
((("Anne" "is" "rough" "+")) -> ("Anne" "is" "quiet" "+"))
If something is young and not kind then it is blue.
((("something" "is" "young" "+") ("something" "is" "kind" "~")) -> ("something" "is" "blue" "+"))
Green things are not big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "-"))
If Anne is not blue and Anne is not green then Anne is big.
((("Anne" "is" "blue" "~") ("Anne" "is" "green" "~")) -> ("Anne" "is" "big" "+"))
Anne is young.
True
1
proof
[(triple4)]
("Anne" "is" "young" "+")
triple4
Gary is big.
False
1
inv-proof
[(triple9 OR ((triple11) -> rule7))]
("Gary" "is" "big" "+")
triple9
((triple11) -> (rule7 % int1))
Gary is not big.
("Gary" "is" "big" "-")
int1
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "blue" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Anne is green.[(triple1)] Anne is quiet.[(triple2 OR ((triple3) -> rule5) OR ((((triple1 triple4) -> rule4)) -> rule5) OR ((((triple4 triple1) -> rule3)) -> rule5))] Anne is rough.[(triple3 OR ((triple1 triple4) -> rule4) OR ((triple4 triple1) -> rule3))] Anne is young.[(triple4)] Bob is big.[(triple5)] Bob is blue.[(triple6)] Bob is kind.[(triple7)] Bob is young.[(triple8)] Gary is blue.[(triple10)] Gary is green.[(triple11)] Gary is kind.[(triple12)] Gary is not big.[(triple9 OR ((triple11) -> rule7))] Gary is not young.[(triple15)] Gary is quiet.[(triple13)] Gary is rough.[(triple14 OR ((triple10) -> rule2))] @1: Anne is not big.[(((triple1) -> rule7))] Bob is rough.[(((triple6) -> rule2))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
((triple3) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple1 triple4) -> (rule4 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((((triple4 triple1) -> (rule3 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
((triple1 triple4) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple4 triple1) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple4
Bob is big.
("Bob" "is" "big" "+")
triple5
Bob is blue.
("Bob" "is" "blue" "+")
triple6
Bob is kind.
("Bob" "is" "kind" "+")
triple7
Bob is young.
("Bob" "is" "young" "+")
triple8
Gary is blue.
("Gary" "is" "blue" "+")
triple10
Gary is green.
("Gary" "is" "green" "+")
triple11
Gary is kind.
("Gary" "is" "kind" "+")
triple12
Gary is not big.
("Gary" "is" "big" "-")
triple9
((triple11) -> (rule7 % int1))
Gary is not big.
("Gary" "is" "big" "-")
int1
Gary is not young.
("Gary" "is" "young" "-")
triple15
Gary is quiet.
("Gary" "is" "quiet" "+")
triple13
Gary is rough.
("Gary" "is" "rough" "+")
triple14
((triple10) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Anne is not big.
("Anne" "is" "big" "-")
((triple1) -> (rule7 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((triple6) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1