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