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