Dave is cold. Dave is kind. Fiona is blue. Fiona is green. Gary is cold. Gary is green. Gary is rough. If Fiona is green and Fiona is round then Fiona is kind. If Dave is cold then Dave is big. Big, kind people are green. Green people are rough. If Gary is big then Gary is cold. All round, cold people are green. If someone is big then they are round. If Gary is round and Gary is rough then Gary is cold.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If Fiona is green and Fiona is round then Fiona is kind.
((("Fiona" "is" "green" "+") ("Fiona" "is" "round" "+")) -> ("Fiona" "is" "kind" "+"))
If Dave is cold then Dave is big.
((("Dave" "is" "cold" "+")) -> ("Dave" "is" "big" "+"))
Big, kind people are green.
((("someone" "is" "big" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
Green people are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If Gary is big then Gary is cold.
((("Gary" "is" "big" "+")) -> ("Gary" "is" "cold" "+"))
All round, cold people are green.
((("someone" "is" "round" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
If someone is big then they are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If Gary is round and Gary is rough then Gary is cold.
((("Gary" "is" "round" "+") ("Gary" "is" "rough" "+")) -> ("Gary" "is" "cold" "+"))
Gary is rough.
True
1
proof
[(triple7 OR ((triple6) -> rule4))]
("Gary" "is" "rough" "+")
triple7
((triple6) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Dave is not kind.
False
1
inv-proof
[(triple2)]
("Dave" "is" "kind" "-")
triple2
Dave is big.
True
2
proof
[(((triple1) -> rule2))]
("Dave" "is" "big" "+")
((triple1) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not big.
False
2
inv-proof
[(((triple1) -> rule2))]
("Dave" "is" "big" "-")
((triple1) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
True
4
proof
[(((((triple1) -> rule2) triple2) -> rule3) OR ((((((triple1) -> rule2)) -> rule7) triple1) -> rule6))]
("Dave" "is" "green" "+")
((((triple1) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule7 % int2)) triple1) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is not round.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule7))]
("Dave" "is" "round" "-")
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is rough.
True
5
proof
[(((((((triple1) -> rule2) triple2) -> rule3)) -> rule4) OR ((((((((triple1) -> rule2)) -> rule7) triple1) -> rule6)) -> rule4))]
("Dave" "is" "rough" "+")
((((((triple1) -> (rule2 % int3)) triple2) -> (rule3 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((((((((triple1) -> (rule2 % int4))) -> (rule7 % int3)) triple1) -> (rule6 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is not rough.
False
5
inv-proof
[(((((((triple1) -> rule2) triple2) -> rule3)) -> rule4) OR ((((((((triple1) -> rule2)) -> rule7) triple1) -> rule6)) -> rule4))]
("Dave" "is" "rough" "-")
((((((triple1) -> (rule2 % int3)) triple2) -> (rule3 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((((((((triple1) -> (rule2 % int4))) -> (rule7 % int3)) triple1) -> (rule6 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Fiona" "is" "round" "-")
Gary is round.
Unknown
rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "round" "+")
Fiona is not kind.
Unknown
inv-rconc
[@2: Fiona is kind.[CWA. Example of deepest failure = (rule1 <- rule7 <- FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Dave is cold.[(triple1)] Dave is kind.[(triple2)] Fiona is blue.[(triple3)] Fiona is green.[(triple4)] Gary is cold.[(triple5)] Gary is green.[(triple6)] Gary is rough.[(triple7 OR ((triple6) -> rule4))] @1: Dave is big.[(((triple1) -> rule2))] Fiona is rough.[(((triple4) -> rule4))] @2: Dave is green.[(((((triple1) -> rule2) triple2) -> rule3) OR ((((((triple1) -> rule2)) -> rule7) triple1) -> rule6))] Dave is round.[(((((triple1) -> rule2)) -> rule7))] @3: Dave is rough.[(((((((triple1) -> rule2) triple2) -> rule3)) -> rule4) OR ((((((((triple1) -> rule2)) -> rule7) triple1) -> rule6)) -> rule4))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Fiona is blue.
("Fiona" "is" "blue" "+")
triple3
Fiona is green.
("Fiona" "is" "green" "+")
triple4
Gary is cold.
("Gary" "is" "cold" "+")
triple5
Gary is green.
("Gary" "is" "green" "+")
triple6
Gary is rough.
("Gary" "is" "rough" "+")
triple7
((triple6) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple1) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple4) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((((triple1) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule7 % int2)) triple1) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((((triple1) -> (rule2 % int3)) triple2) -> (rule3 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((((((((triple1) -> (rule2 % int4))) -> (rule7 % int3)) triple1) -> (rule6 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4