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