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