Dave is big. Dave is quiet. Dave is round. Erin is big. Erin is cold. Erin is nice. Erin is quiet. Erin is rough. Gary is big. Gary is cold. Gary is kind. Gary is nice. Gary is quiet. Gary is rough. Gary is round. Cold things are nice. Round things are rough. All big things are cold.
Dave is big.
("Dave" "is" "big" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Cold things are nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
Round things are rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
All big things are cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
Gary is rough.
True
1
proof
[(triple14 OR ((triple15) -> rule2))]
("Gary" "is" "rough" "+")
triple14
((triple15) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Dave is not quiet.
False
1
inv-proof
[(triple2)]
("Dave" "is" "quiet" "-")
triple2
Dave is cold.
True
2
proof
[(((triple1) -> rule3))]
("Dave" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple3) -> rule2))]
("Dave" "is" "rough" "-")
((triple3) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
@0: Dave is big.[(triple1)] Dave is quiet.[(triple2)] Dave is round.[(triple3)] Erin is big.[(triple4)] Erin is cold.[(triple5 OR ((triple4) -> rule3))] Erin is nice.[(triple6 OR ((triple5) -> rule1) OR ((((triple4) -> rule3)) -> rule1))] Erin is quiet.[(triple7)] Erin is rough.[(triple8)] Gary is big.[(triple9)] Gary is cold.[(triple10 OR ((triple9) -> rule3))] Gary is kind.[(triple11)] Gary is nice.[(triple12 OR ((triple10) -> rule1) OR ((((triple9) -> rule3)) -> rule1))] Gary is quiet.[(triple13)] Gary is rough.[(triple14 OR ((triple15) -> rule2))] Gary is round.[(triple15)] @1: Dave is cold.[(((triple1) -> rule3))] Dave is rough.[(((triple3) -> rule2))] @2: Dave is nice.[(((((triple1) -> rule3)) -> rule1))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
Erin is cold.
("Erin" "is" "cold" "+")
triple5
((triple4) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple6
((triple5) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple7
Erin is rough.
("Erin" "is" "rough" "+")
triple8
Gary is big.
("Gary" "is" "big" "+")
triple9
Gary is cold.
("Gary" "is" "cold" "+")
triple10
((triple9) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple11
Gary is nice.
("Gary" "is" "nice" "+")
triple12
((triple10) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple9) -> (rule3 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple13
Gary is rough.
("Gary" "is" "rough" "+")
triple14
((triple15) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
triple15
Dave is cold.
("Dave" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple3) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2