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