Dave is white. Erin is smart. Erin is young. Gary is cold. Gary is nice. Gary is smart. Gary is young. White, smart things are young. If Gary is cold and Gary is white then Gary is not round. If something is rough then it is smart. If something is smart then it is white. If something is round then it is not cold. All smart things are cold. White things are rough. If Erin is not rough then Erin is young.
Dave is white.
("Dave" "is" "white" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
White, smart things are young.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
If Gary is cold and Gary is white then Gary is not round.
((("Gary" "is" "cold" "+") ("Gary" "is" "white" "+")) -> ("Gary" "is" "round" "-"))
If something is rough then it is smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
If something is smart then it is white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
If something is round then it is not cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "-"))
All smart things are cold.
((("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
White things are rough.
((("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
If Erin is not rough then Erin is young.
((("Erin" "is" "rough" "~")) -> ("Erin" "is" "young" "+"))
Gary is smart.
True
1
proof
[(triple6)]
("Gary" "is" "smart" "+")
triple6
Dave is not white.
False
1
inv-proof
[(triple1)]
("Dave" "is" "white" "-")
triple1
Gary is white.
True
2
proof
[(((triple6) -> rule4))]
("Gary" "is" "white" "+")
((triple6) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple1) -> rule7))]
("Dave" "is" "rough" "-")
((triple1) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
True
3
proof
[(((((triple1) -> rule7)) -> rule3))]
("Dave" "is" "smart" "+")
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Erin is not rough.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule7))]
("Erin" "is" "rough" "-")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Dave is cold.
True
4
proof
[(((((((triple1) -> rule7)) -> rule3)) -> rule6))]
("Dave" "is" "cold" "+")
((((((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is not young.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule7)) -> rule3)) -> rule1))]
("Dave" "is" "young" "-")
((triple1 ((((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Dave is white.[(triple1)] Erin is smart.[(triple2)] Erin is young.[(triple3 OR ((((triple2) -> rule4) triple2) -> rule1))] Gary is cold.[(triple4 OR ((triple6) -> rule6))] Gary is nice.[(triple5)] Gary is smart.[(triple6)] Gary is young.[(triple7 OR ((((triple6) -> rule4) triple6) -> rule1))] @1: Dave is rough.[(((triple1) -> rule7))] Erin is cold.[(((triple2) -> rule6))] Erin is white.[(((triple2) -> rule4))] Gary is white.[(((triple6) -> rule4))] @2: Dave is smart.[(((((triple1) -> rule7)) -> rule3))] Erin is rough.[(((((triple2) -> rule4)) -> rule7))] Gary is not round.[(((triple4 ((triple6) -> rule4)) -> rule2) OR ((((triple6) -> rule6) ((triple6) -> rule4)) -> rule2))] Gary is rough.[(((((triple6) -> rule4)) -> rule7))] @3: Dave is cold.[(((((((triple1) -> rule7)) -> rule3)) -> rule6))] Dave is young.[(((triple1 ((((triple1) -> rule7)) -> rule3)) -> rule1))]
Dave is white.
("Dave" "is" "white" "+")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
((((triple2) -> (rule4 % int2)) triple2) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
triple4
((triple6) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple5
Gary is smart.
("Gary" "is" "smart" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
((((triple6) -> (rule4 % int2)) triple6) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((triple1) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple2) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple2) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple6) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Gary is not round.
("Gary" "is" "round" "-")
((triple4 ((triple6) -> (rule4 % int2))) -> (rule2 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((((triple6) -> (rule6 % int3)) ((triple6) -> (rule4 % int2))) -> (rule2 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
((((triple6) -> (rule4 % int2))) -> (rule7 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((((((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
((triple1 ((((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3