Bob is not cold. Bob is green. Bob is nice. Bob is quiet. Bob is red. Charlie is cold. Charlie is furry. Charlie is green. Charlie is not quiet. Charlie is red. Charlie is rough. Harry is furry. Harry is green. Harry is quiet. Harry is rough. If someone is furry then they are nice. If someone is red and not cold then they are nice. If someone is rough and nice then they are red.
Bob is not cold.
("Bob" "is" "cold" "-")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If someone is furry then they are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
If someone is red and not cold then they are nice.
((("someone" "is" "red" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "nice" "+"))
If someone is rough and nice then they are red.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
Charlie is not quiet.
True
1
proof
[(triple9)]
("Charlie" "is" "quiet" "-")
triple9
Harry is not green.
False
1
inv-proof
[(triple13)]
("Harry" "is" "green" "-")
triple13
Harry is nice.
True
2
proof
[(((triple12) -> rule1))]
("Harry" "is" "nice" "+")
((triple12) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not nice.
False
2
inv-proof
[(((triple12) -> rule1))]
("Harry" "is" "nice" "-")
((triple12) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
True
4
proof
[(((triple15 ((triple12) -> rule1)) -> rule3))]
("Harry" "is" "red" "+")
((triple15 ((triple12) -> (rule1 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not red.
False
4
inv-proof
[(((triple15 ((triple12) -> rule1)) -> rule3))]
("Harry" "is" "red" "-")
((triple15 ((triple12) -> (rule1 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Bob is green.[(triple2)] Bob is nice.[(triple3 OR ((triple5 triple1) -> rule2))] Bob is not cold.[(triple1)] Bob is quiet.[(triple4)] Bob is red.[(triple5)] Charlie is cold.[(triple6)] Charlie is furry.[(triple7)] Charlie is green.[(triple8)] Charlie is not quiet.[(triple9)] Charlie is red.[(triple10 OR ((triple11 ((triple7) -> rule1)) -> rule3))] Charlie is rough.[(triple11)] Harry is furry.[(triple12)] Harry is green.[(triple13)] Harry is quiet.[(triple14)] Harry is rough.[(triple15)] @1: Charlie is nice.[(((triple7) -> rule1))] Harry is nice.[(((triple12) -> rule1))] @2: Harry is red.[(((triple15 ((triple12) -> rule1)) -> rule3))]
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
((triple5 triple1) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not cold.
("Bob" "is" "cold" "-")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
Charlie is cold.
("Charlie" "is" "cold" "+")
triple6
Charlie is furry.
("Charlie" "is" "furry" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
triple8
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple9
Charlie is red.
("Charlie" "is" "red" "+")
triple10
((triple11 ((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple11
Harry is furry.
("Harry" "is" "furry" "+")
triple12
Harry is green.
("Harry" "is" "green" "+")
triple13
Harry is quiet.
("Harry" "is" "quiet" "+")
triple14
Harry is rough.
("Harry" "is" "rough" "+")
triple15
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple7) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple12) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple15 ((triple12) -> (rule1 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2