Anne is nice. Anne is young. Dave is cold. Dave is rough. Dave is smart. Fiona is big. Gary is big. All young people are rough. If someone is rough and smart then they are cold. If Anne is rough then Anne is smart. If someone is cold then they are big. All smart people are nice. Round people are young. Young, cold people are rough. Cold, big people are round.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Gary is big.
("Gary" "is" "big" "+")
All young people are rough.
((("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
If someone is rough and smart then they are cold.
((("someone" "is" "rough" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
If Anne is rough then Anne is smart.
((("Anne" "is" "rough" "+")) -> ("Anne" "is" "smart" "+"))
If someone is cold then they are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
All smart people are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
Round people are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
Young, cold people are rough.
((("someone" "is" "young" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
Cold, big people are round.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
Dave is cold.
True
1
proof
[(triple3 OR ((triple4 triple5) -> rule2))]
("Dave" "is" "cold" "+")
triple3
((triple4 triple5) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not rough.
False
1
inv-proof
[(triple4 OR ((((((triple3 ((triple3) -> rule4)) -> rule8)) -> rule6)) -> rule1) OR ((((((triple3 ((triple3) -> rule4)) -> rule8)) -> rule6) triple3) -> rule7))]
("Dave" "is" "rough" "-")
triple4
((((((triple3 ((triple3) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
((((((triple3 ((triple3) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule6 % int2)) triple3) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Anne is rough.
True
2
proof
[(((triple2) -> rule1))]
("Anne" "is" "rough" "+")
((triple2) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not rough.
False
2
inv-proof
[(((triple2) -> rule1))]
("Anne" "is" "rough" "-")
((triple2) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Dave is round.
True
4
proof
[(((triple3 ((triple3) -> rule4)) -> rule8) OR ((((triple4 triple5) -> rule2) ((triple3) -> rule4)) -> rule8) OR ((triple3 ((((triple4 triple5) -> rule2)) -> rule4)) -> rule8) OR ((((triple4 triple5) -> rule2) ((((triple4 triple5) -> rule2)) -> rule4)) -> rule8))]
("Dave" "is" "round" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((triple4 triple5) -> (rule2 % int3)) ((triple3) -> (rule4 % int2))) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
((triple3 ((((triple4 triple5) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
((((triple4 triple5) -> (rule2 % int3)) ((((triple4 triple5) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Anne is not smart.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("Anne" "is" "smart" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Dave is young.
True
5
proof
[(((((triple3 ((triple3) -> rule4)) -> rule8)) -> rule6) OR ((((((triple4 triple5) -> rule2) ((triple3) -> rule4)) -> rule8)) -> rule6) OR ((((triple3 ((((triple4 triple5) -> rule2)) -> rule4)) -> rule8)) -> rule6) OR ((((((triple4 triple5) -> rule2) ((((triple4 triple5) -> rule2)) -> rule4)) -> rule8)) -> rule6))]
("Dave" "is" "young" "+")
((((triple3 ((triple3) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((((((triple4 triple5) -> (rule2 % int4)) ((triple3) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
((((triple3 ((((triple4 triple5) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
((((((triple4 triple5) -> (rule2 % int4)) ((((triple4 triple5) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
Anne is not cold.
False
6
inv-proof
[(((((triple2) -> rule1) ((((triple2) -> rule1)) -> rule3)) -> rule2))]
("Anne" "is" "cold" "-")
((((triple2) -> (rule1 % int3)) ((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is big.
True
7
proof
[(((((((triple2) -> rule1) ((((triple2) -> rule1)) -> rule3)) -> rule2)) -> rule4))]
("Anne" "is" "big" "+")
((((((triple2) -> (rule1 % int4)) ((((triple2) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4
Anne is not big.
False
7
inv-proof
[(((((((triple2) -> rule1) ((((triple2) -> rule1)) -> rule3)) -> rule2)) -> rule4))]
("Anne" "is" "big" "-")
((((((triple2) -> (rule1 % int4)) ((((triple2) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4
Anne is round.
True
14
proof
[(((((((triple2) -> rule1) ((((triple2) -> rule1)) -> rule3)) -> rule2) ((((((triple2) -> rule1) ((((triple2) -> rule1)) -> rule3)) -> rule2)) -> rule4)) -> rule8))]
("Anne" "is" "round" "+")
((((((triple2) -> (rule1 % int5)) ((((triple2) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule2 % int3)) ((((((triple2) -> (rule1 % int5)) ((((triple2) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is rough.
("Anne" "is" "rough" "+")
int5
Anne is not round.
False
14
inv-proof
[(((((((triple2) -> rule1) ((((triple2) -> rule1)) -> rule3)) -> rule2) ((((((triple2) -> rule1) ((((triple2) -> rule1)) -> rule3)) -> rule2)) -> rule4)) -> rule8))]
("Anne" "is" "round" "-")
((((((triple2) -> (rule1 % int5)) ((((triple2) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule2 % int3)) ((((((triple2) -> (rule1 % int5)) ((((triple2) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is rough.
("Anne" "is" "rough" "+")
int5
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "cold" "-")
Fiona is nice.
Unknown
rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "nice" "+")
Gary is not young.
Unknown
inv-rconc
[@3: Gary is young.[CWA. Example of deepest failure = (rule6 <- rule8 <- rule2 <- FAIL)]]
("Gary" "is" "young" "-")
Gary is rough.
Unknown
rconc
[@4: Gary is rough.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule8 <- rule2 <- FAIL)]]
("Gary" "is" "rough" "+")
Fiona is not round.
Unknown
inv-rconc
[@2: Fiona is round.[CWA. Example of deepest failure = (rule8 <- rule2 <- FAIL)]]
("Fiona" "is" "round" "-")
Fiona is rough.
Unknown
rconc
[@4: Fiona is rough.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule8 <- rule2 <- FAIL)]]
("Fiona" "is" "rough" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Anne is nice.[(triple1 OR ((((((triple2) -> rule1)) -> rule3)) -> rule5))] Anne is young.[(triple2)] Dave is cold.[(triple3 OR ((triple4 triple5) -> rule2))] Dave is rough.[(triple4 OR ((((((triple3 ((triple3) -> rule4)) -> rule8)) -> rule6)) -> rule1) OR ((((((triple3 ((triple3) -> rule4)) -> rule8)) -> rule6) triple3) -> rule7))] Dave is smart.[(triple5)] Fiona is big.[(triple6)] Gary is big.[(triple7)] @1: Anne is rough.[(((triple2) -> rule1))] Dave is big.[(((triple3) -> rule4) OR ((((triple4 triple5) -> rule2)) -> rule4))] Dave is nice.[(((triple5) -> rule5))] @2: Anne is smart.[(((((triple2) -> rule1)) -> rule3))] Dave is round.[(((triple3 ((triple3) -> rule4)) -> rule8) OR ((((triple4 triple5) -> rule2) ((triple3) -> rule4)) -> rule8) OR ((triple3 ((((triple4 triple5) -> rule2)) -> rule4)) -> rule8) OR ((((triple4 triple5) -> rule2) ((((triple4 triple5) -> rule2)) -> rule4)) -> rule8))] @3: Anne is cold.[(((((triple2) -> rule1) ((((triple2) -> rule1)) -> rule3)) -> rule2))] Dave is young.[(((((triple3 ((triple3) -> rule4)) -> rule8)) -> rule6) OR ((((((triple4 triple5) -> rule2) ((triple3) -> rule4)) -> rule8)) -> rule6) OR ((((triple3 ((((triple4 triple5) -> rule2)) -> rule4)) -> rule8)) -> rule6) OR ((((((triple4 triple5) -> rule2) ((((triple4 triple5) -> rule2)) -> rule4)) -> rule8)) -> rule6))] @4: Anne is big.[(((((((triple2) -> rule1) ((((triple2) -> rule1)) -> rule3)) -> rule2)) -> rule4))] @5: Anne is round.[(((((((triple2) -> rule1) ((((triple2) -> rule1)) -> rule3)) -> rule2) ((((((triple2) -> rule1) ((((triple2) -> rule1)) -> rule3)) -> rule2)) -> rule4)) -> rule8))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
((triple4 triple5) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple4
((((((triple3 ((triple3) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
((((((triple3 ((triple3) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule6 % int2)) triple3) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Fiona is big.
("Fiona" "is" "big" "+")
triple6
Gary is big.
("Gary" "is" "big" "+")
triple7
Anne is rough.
("Anne" "is" "rough" "+")
((triple2) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple3) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((triple4 triple5) -> (rule2 % int2))) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((triple5) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((triple4 triple5) -> (rule2 % int3)) ((triple3) -> (rule4 % int2))) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
((triple3 ((((triple4 triple5) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
((((triple4 triple5) -> (rule2 % int3)) ((((triple4 triple5) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
((((triple2) -> (rule1 % int3)) ((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
((((triple3 ((triple3) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((((((triple4 triple5) -> (rule2 % int4)) ((triple3) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
((((triple3 ((((triple4 triple5) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
((((((triple4 triple5) -> (rule2 % int4)) ((((triple4 triple5) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
Anne is big.
("Anne" "is" "big" "+")
((((((triple2) -> (rule1 % int4)) ((((triple2) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
((((((triple2) -> (rule1 % int5)) ((((triple2) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule2 % int3)) ((((((triple2) -> (rule1 % int5)) ((((triple2) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is rough.
("Anne" "is" "rough" "+")
int5