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