Bob is blue. Bob is green. Bob is kind. Bob is nice. Bob is quiet. Bob is round. Harry is blue. Harry is green. Harry is quiet. Harry is round. If someone is blue and green then they are kind. All quiet people are kind. Green people are nice. Nice, blue people are green. If Bob is nice then Bob is kind. Green, nice people are quiet. Cold people are quiet. All blue, cold people are round.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
If someone is blue and green then they are kind.
((("someone" "is" "blue" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
All quiet people are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
Green people are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Nice, blue people are green.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
If Bob is nice then Bob is kind.
((("Bob" "is" "nice" "+")) -> ("Bob" "is" "kind" "+"))
Green, nice people are quiet.
((("someone" "is" "green" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
Cold people are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
All blue, cold people are round.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
Harry is quiet.
True
1
proof
[(triple9 OR ((triple8 ((triple8) -> rule3)) -> rule6))]
("Harry" "is" "quiet" "+")
triple9
((triple8 ((triple8) -> (rule3 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not round.
False
1
inv-proof
[(triple10)]
("Harry" "is" "round" "-")
triple10
Harry is kind.
True
2
proof
[(((triple9) -> rule2) OR ((triple7 triple8) -> rule1) OR ((((triple8 ((triple8) -> rule3)) -> rule6)) -> rule2))]
("Harry" "is" "kind" "+")
((triple9) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple7 triple8) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple8 ((triple8) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is not nice.
False
2
inv-proof
[(((triple8) -> rule3))]
("Harry" "is" "nice" "-")
((triple8) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Bob is blue.[(triple1)] Bob is green.[(triple2 OR ((triple4 triple1) -> rule4))] Bob is kind.[(triple3 OR ((triple4) -> rule5) OR ((triple5) -> rule2) OR ((triple1 triple2) -> rule1) OR ((((triple2) -> rule3)) -> rule5) OR ((((triple2 triple4) -> rule6)) -> rule2) OR ((triple1 ((triple4 triple1) -> rule4)) -> rule1) OR ((((triple2 ((triple2) -> rule3)) -> rule6)) -> rule2) OR ((((((triple4 triple1) -> rule4) triple4) -> rule6)) -> rule2) OR ((((((triple4 triple1) -> rule4) ((triple2) -> rule3)) -> rule6)) -> rule2))] Bob is nice.[(triple4 OR ((triple2) -> rule3))] Bob is quiet.[(triple5 OR ((triple2 triple4) -> rule6) OR ((triple2 ((triple2) -> rule3)) -> rule6) OR ((((triple4 triple1) -> rule4) triple4) -> rule6) OR ((((triple4 triple1) -> rule4) ((triple2) -> rule3)) -> rule6))] Bob is round.[(triple6)] Harry is blue.[(triple7)] Harry is green.[(triple8)] Harry is quiet.[(triple9 OR ((triple8 ((triple8) -> rule3)) -> rule6))] Harry is round.[(triple10)] @1: Harry is kind.[(((triple9) -> rule2) OR ((triple7 triple8) -> rule1) OR ((((triple8 ((triple8) -> rule3)) -> rule6)) -> rule2))] Harry is nice.[(((triple8) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
((triple4 triple1) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple4) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple5) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple1 triple2) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple2 triple4) -> (rule6 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((triple1 ((triple4 triple1) -> (rule4 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
((((((triple4 triple1) -> (rule4 % int3)) triple4) -> (rule6 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((((triple4 triple1) -> (rule4 % int4)) ((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is nice.
("Bob" "is" "nice" "+")
triple4
((triple2) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
((triple2 triple4) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple2 ((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple4 triple1) -> (rule4 % int2)) triple4) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple4 triple1) -> (rule4 % int3)) ((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
triple6
Harry is blue.
("Harry" "is" "blue" "+")
triple7
Harry is green.
("Harry" "is" "green" "+")
triple8
Harry is quiet.
("Harry" "is" "quiet" "+")
triple9
((triple8 ((triple8) -> (rule3 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
triple10
Harry is kind.
("Harry" "is" "kind" "+")
((triple9) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple7 triple8) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple8 ((triple8) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
((triple8) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1