Anne is big. Anne is blue. Anne is nice. Anne is young. Bob is blue. Bob is green. Bob is nice. Bob is quiet. Bob is red. Harry is not blue. Harry is quiet. Harry is young. If something is nice then it is quiet. If something is nice and not blue then it is not big. If Anne is quiet then Anne is red. If something is nice and not big then it is green. All nice things are green. If something is nice then it is green. If something is young and not nice then it is red. If something is green and not big then it is red.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Harry is not blue.
("Harry" "is" "blue" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is nice then it is quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
If something is nice and not blue then it is not big.
((("something" "is" "nice" "+") ("something" "is" "blue" "~")) -> ("something" "is" "big" "-"))
If Anne is quiet then Anne is red.
((("Anne" "is" "quiet" "+")) -> ("Anne" "is" "red" "+"))
If something is nice and not big then it is green.
((("something" "is" "nice" "+") ("something" "is" "big" "~")) -> ("something" "is" "green" "+"))
All nice things are green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If something is nice then it is green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If something is young and not nice then it is red.
((("something" "is" "young" "+") ("something" "is" "nice" "~")) -> ("something" "is" "red" "+"))
If something is green and not big then it is red.
((("something" "is" "green" "+") ("something" "is" "big" "~")) -> ("something" "is" "red" "+"))
Harry is quiet.
True
1
proof
[(triple11)]
("Harry" "is" "quiet" "+")
triple11
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Anne is green.
True
2
proof
[(((triple3) -> rule5) OR ((triple3) -> rule6))]
("Anne" "is" "green" "+")
((triple3) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple3) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is not quiet.
False
2
inv-proof
[(((triple3) -> rule1))]
("Anne" "is" "quiet" "-")
((triple3) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
True
3
proof
[(((((triple3) -> rule1)) -> rule3))]
("Anne" "is" "red" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not red.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule3))]
("Anne" "is" "red" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "red" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "green" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is nice.[(triple3)] Anne is young.[(triple4)] Bob is blue.[(triple5)] Bob is green.[(triple6 OR ((triple7) -> rule5) OR ((triple7) -> rule6))] Bob is nice.[(triple7)] Bob is quiet.[(triple8 OR ((triple7) -> rule1))] Bob is red.[(triple9)] Harry is not blue.[(triple10)] Harry is quiet.[(triple11)] Harry is young.[(triple12)] @1: Anne is green.[(((triple3) -> rule5) OR ((triple3) -> rule6))] Anne is quiet.[(((triple3) -> rule1))] @2: Anne is red.[(((((triple3) -> rule1)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple4
Bob is blue.
("Bob" "is" "blue" "+")
triple5
Bob is green.
("Bob" "is" "green" "+")
triple6
((triple7) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((triple7) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
triple7
Bob is quiet.
("Bob" "is" "quiet" "+")
triple8
((triple7) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple9
Harry is not blue.
("Harry" "is" "blue" "-")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
Anne is green.
("Anne" "is" "green" "+")
((triple3) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple3) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple3) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2