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