Erin is big. Erin is blue. Erin is green. Erin is round. Gary is big. Gary is round. Gary is white. All white things are quiet. All white things are round. If something is quiet then it is big. If Erin is green then Erin is white. Green things are smart. Quiet things are smart.
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is round.
("Erin" "is" "round" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
All white things are quiet.
((("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
All white things are round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
If something is quiet then it is big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
If Erin is green then Erin is white.
((("Erin" "is" "green" "+")) -> ("Erin" "is" "white" "+"))
Green things are smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
Quiet things are smart.
((("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
Gary is round.
True
1
proof
[(triple6 OR ((triple7) -> rule2))]
("Gary" "is" "round" "+")
triple6
((triple7) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is not big.
False
1
inv-proof
[(triple5 OR ((((triple7) -> rule1)) -> rule3))]
("Gary" "is" "big" "-")
triple5
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Erin is big.[(triple1 OR ((((((triple3) -> rule4)) -> rule1)) -> rule3))] Erin is blue.[(triple2)] Erin is green.[(triple3)] Erin is round.[(triple4 OR ((((triple3) -> rule4)) -> rule2))] Gary is big.[(triple5 OR ((((triple7) -> rule1)) -> rule3))] Gary is round.[(triple6 OR ((triple7) -> rule2))] Gary is white.[(triple7)] @1: Erin is smart.[(((triple3) -> rule5) OR ((((((triple3) -> rule4)) -> rule1)) -> rule6))] Erin is white.[(((triple3) -> rule4))] Gary is quiet.[(((triple7) -> rule1))] @2: Erin is quiet.[(((((triple3) -> rule4)) -> rule1))] Gary is smart.[(((((triple7) -> rule1)) -> rule6))]
Erin is big.
("Erin" "is" "big" "+")
triple1
((((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Erin is green.
("Erin" "is" "green" "+")
triple3
Erin is round.
("Erin" "is" "round" "+")
triple4
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
triple5
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
triple6
((triple7) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple7
Erin is smart.
("Erin" "is" "smart" "+")
((triple3) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
((triple3) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple7) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((triple7) -> (rule1 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2