Bob is green. Bob is nice. Bob is red. Bob is white. Gary is cold. Gary is green. Gary is nice. Gary is red. Gary is rough. Harry is cold. Harry is green. Harry is nice. Harry is red. Harry is rough. Harry is white. Harry is young. If something is white and green then it is young. All rough, nice things are white.
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is white and green then it is young.
((("something" "is" "white" "+") ("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
All rough, nice things are white.
((("something" "is" "rough" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
Harry is young.
True
1
proof
[(triple16 OR ((triple15 triple11) -> rule1) OR ((((triple14 triple12) -> rule2) triple11) -> rule1))]
("Harry" "is" "young" "+")
triple16
((triple15 triple11) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple14 triple12) -> (rule2 % int2)) triple11) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Bob is not white.
False
1
inv-proof
[(triple4)]
("Bob" "is" "white" "-")
triple4
Gary is white.
True
3
proof
[(((triple9 triple7) -> rule2))]
("Gary" "is" "white" "+")
((triple9 triple7) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Bob is not young.
False
3
inv-proof
[(((triple4 triple1) -> rule1))]
("Bob" "is" "young" "-")
((triple4 triple1) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Gary is young.
True
5
proof
[(((((triple9 triple7) -> rule2) triple6) -> rule1))]
("Gary" "is" "young" "+")
((((triple9 triple7) -> (rule2 % int2)) triple6) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is not young.
False
5
inv-proof
[(((((triple9 triple7) -> rule2) triple6) -> rule1))]
("Gary" "is" "young" "-")
((((triple9 triple7) -> (rule2 % int2)) triple6) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Bob is green.[(triple1)] Bob is nice.[(triple2)] Bob is red.[(triple3)] Bob is white.[(triple4)] Gary is cold.[(triple5)] Gary is green.[(triple6)] Gary is nice.[(triple7)] Gary is red.[(triple8)] Gary is rough.[(triple9)] Harry is cold.[(triple10)] Harry is green.[(triple11)] Harry is nice.[(triple12)] Harry is red.[(triple13)] Harry is rough.[(triple14)] Harry is white.[(triple15 OR ((triple14 triple12) -> rule2))] Harry is young.[(triple16 OR ((triple15 triple11) -> rule1) OR ((((triple14 triple12) -> rule2) triple11) -> rule1))] @1: Bob is young.[(((triple4 triple1) -> rule1))] Gary is white.[(((triple9 triple7) -> rule2))] @2: Gary is young.[(((((triple9 triple7) -> rule2) triple6) -> rule1))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
Gary is cold.
("Gary" "is" "cold" "+")
triple5
Gary is green.
("Gary" "is" "green" "+")
triple6
Gary is nice.
("Gary" "is" "nice" "+")
triple7
Gary is red.
("Gary" "is" "red" "+")
triple8
Gary is rough.
("Gary" "is" "rough" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
Harry is green.
("Harry" "is" "green" "+")
triple11
Harry is nice.
("Harry" "is" "nice" "+")
triple12
Harry is red.
("Harry" "is" "red" "+")
triple13
Harry is rough.
("Harry" "is" "rough" "+")
triple14
Harry is white.
("Harry" "is" "white" "+")
triple15
((triple14 triple12) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple16
((triple15 triple11) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple14 triple12) -> (rule2 % int2)) triple11) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((triple4 triple1) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple9 triple7) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((((triple9 triple7) -> (rule2 % int2)) triple6) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2