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