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