Bob is blue. Harry is blue. Harry is cold. Harry is furry. Harry is nice. Harry is red. Harry is round. If something is red then it is nice. Blue things are red.
Bob is blue.
("Bob" "is" "blue" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
If something is red then it is nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
Blue things are red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
Harry is blue.
True
1
proof
[(triple2)]
("Harry" "is" "blue" "+")
triple2
Harry is not red.
False
1
inv-proof
[(triple6 OR ((triple2) -> rule2))]
("Harry" "is" "red" "-")
triple6
((triple2) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Bob is red.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "red" "+")
((triple1) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not red.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "red" "-")
((triple1) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is nice.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("Bob" "is" "nice" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is not nice.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("Bob" "is" "nice" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Bob is blue.[(triple1)] Harry is blue.[(triple2)] Harry is cold.[(triple3)] Harry is furry.[(triple4)] Harry is nice.[(triple5 OR ((triple6) -> rule1) OR ((((triple2) -> rule2)) -> rule1))] Harry is red.[(triple6 OR ((triple2) -> rule2))] Harry is round.[(triple7)] @1: Bob is red.[(((triple1) -> rule2))] @2: Bob is nice.[(((((triple1) -> rule2)) -> rule1))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Harry is blue.
("Harry" "is" "blue" "+")
triple2
Harry is cold.
("Harry" "is" "cold" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
triple4
Harry is nice.
("Harry" "is" "nice" "+")
triple5
((triple6) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
triple6
((triple2) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple7
Bob is red.
("Bob" "is" "red" "+")
((triple1) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2