Anne is furry. Anne is nice. Anne is rough. Anne is young. Charlie is big. Charlie is cold. Charlie is furry. Charlie is green. Charlie is nice. Charlie is rough. Dave is big. Dave is rough. Fiona is big. Fiona is young. If someone is big and furry then they are nice. All green people are furry. All young, nice people are cold. All young people are rough. All rough, young people are green. All nice, young people are green.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If someone is big and furry then they are nice.
((("someone" "is" "big" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
All green people are furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
All young, nice people are cold.
((("someone" "is" "young" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
All young people are rough.
((("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
All rough, young people are green.
((("someone" "is" "rough" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
All nice, young people are green.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
Anne is nice.
True
1
proof
[(triple2)]
("Anne" "is" "nice" "+")
triple2
Charlie is not rough.
False
1
inv-proof
[(triple10)]
("Charlie" "is" "rough" "-")
triple10
Anne is green.
True
3
proof
[(((triple2 triple4) -> rule6) OR ((triple3 triple4) -> rule5) OR ((((triple4) -> rule4) triple4) -> rule5))]
("Anne" "is" "green" "+")
((triple2 triple4) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple3 triple4) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((((triple4) -> (rule4 % int2)) triple4) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not cold.
False
3
inv-proof
[(((triple4 triple2) -> rule3))]
("Anne" "is" "cold" "-")
((triple4 triple2) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Fiona is green.
True
4
proof
[(((((triple14) -> rule4) triple14) -> rule5))]
("Fiona" "is" "green" "+")
((((triple14) -> (rule4 % int2)) triple14) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is not green.
False
4
inv-proof
[(((((triple14) -> rule4) triple14) -> rule5))]
("Fiona" "is" "green" "-")
((((triple14) -> (rule4 % int2)) triple14) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is furry.
True
5
proof
[(((((((triple14) -> rule4) triple14) -> rule5)) -> rule2))]
("Fiona" "is" "furry" "+")
((((((triple14) -> (rule4 % int3)) triple14) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is not furry.
False
5
inv-proof
[(((((((triple14) -> rule4) triple14) -> rule5)) -> rule2))]
("Fiona" "is" "furry" "-")
((((((triple14) -> (rule4 % int3)) triple14) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is nice.
True
7
proof
[(((triple13 ((((((triple14) -> rule4) triple14) -> rule5)) -> rule2)) -> rule1))]
("Fiona" "is" "nice" "+")
((triple13 ((((((triple14) -> (rule4 % int4)) triple14) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Fiona is not nice.
False
7
inv-proof
[(((triple13 ((((((triple14) -> rule4) triple14) -> rule5)) -> rule2)) -> rule1))]
("Fiona" "is" "nice" "-")
((triple13 ((((((triple14) -> (rule4 % int4)) triple14) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Fiona is cold.
True
9
proof
[(((triple14 ((triple13 ((((((triple14) -> rule4) triple14) -> rule5)) -> rule2)) -> rule1)) -> rule3))]
("Fiona" "is" "cold" "+")
((triple14 ((triple13 ((((((triple14) -> (rule4 % int5)) triple14) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is rough.
("Fiona" "is" "rough" "+")
int5
Fiona is not cold.
False
9
inv-proof
[(((triple14 ((triple13 ((((((triple14) -> rule4) triple14) -> rule5)) -> rule2)) -> rule1)) -> rule3))]
("Fiona" "is" "cold" "-")
((triple14 ((triple13 ((((((triple14) -> (rule4 % int5)) triple14) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is rough.
("Fiona" "is" "rough" "+")
int5
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "green" "-")
Dave is furry.
Unknown
rconc
[@2: Dave is furry.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Dave" "is" "furry" "+")
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "cold" "-")
Dave is nice.
Unknown
rconc
[@3: Dave is nice.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule5 <- FAIL)]]
("Dave" "is" "nice" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is furry.[(triple1 OR ((((triple2 triple4) -> rule6)) -> rule2) OR ((((triple3 triple4) -> rule5)) -> rule2) OR ((((((triple4) -> rule4) triple4) -> rule5)) -> rule2))] Anne is nice.[(triple2)] Anne is rough.[(triple3 OR ((triple4) -> rule4))] Anne is young.[(triple4)] Charlie is big.[(triple5)] Charlie is cold.[(triple6)] Charlie is furry.[(triple7 OR ((triple8) -> rule2))] Charlie is green.[(triple8)] Charlie is nice.[(triple9 OR ((triple5 triple7) -> rule1) OR ((triple5 ((triple8) -> rule2)) -> rule1))] Charlie is rough.[(triple10)] Dave is big.[(triple11)] Dave is rough.[(triple12)] Fiona is big.[(triple13)] Fiona is young.[(triple14)] @1: Anne is cold.[(((triple4 triple2) -> rule3))] Anne is green.[(((triple2 triple4) -> rule6) OR ((triple3 triple4) -> rule5) OR ((((triple4) -> rule4) triple4) -> rule5))] Fiona is rough.[(((triple14) -> rule4))] @2: Fiona is green.[(((((triple14) -> rule4) triple14) -> rule5))] @3: Fiona is furry.[(((((((triple14) -> rule4) triple14) -> rule5)) -> rule2))] @4: Fiona is nice.[(((triple13 ((((((triple14) -> rule4) triple14) -> rule5)) -> rule2)) -> rule1))] @5: Fiona is cold.[(((triple14 ((triple13 ((((((triple14) -> rule4) triple14) -> rule5)) -> rule2)) -> rule1)) -> rule3))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
((((triple2 triple4) -> (rule6 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((triple3 triple4) -> (rule5 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((((triple4) -> (rule4 % int3)) triple4) -> (rule5 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
((triple4) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple4
Charlie is big.
("Charlie" "is" "big" "+")
triple5
Charlie is cold.
("Charlie" "is" "cold" "+")
triple6
Charlie is furry.
("Charlie" "is" "furry" "+")
triple7
((triple8) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple8
Charlie is nice.
("Charlie" "is" "nice" "+")
triple9
((triple5 triple7) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((triple5 ((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple10
Dave is big.
("Dave" "is" "big" "+")
triple11
Dave is rough.
("Dave" "is" "rough" "+")
triple12
Fiona is big.
("Fiona" "is" "big" "+")
triple13
Fiona is young.
("Fiona" "is" "young" "+")
triple14
Anne is cold.
("Anne" "is" "cold" "+")
((triple4 triple2) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((triple2 triple4) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple3 triple4) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((((triple4) -> (rule4 % int2)) triple4) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple14) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((((triple14) -> (rule4 % int2)) triple14) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
((((((triple14) -> (rule4 % int3)) triple14) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple13 ((((((triple14) -> (rule4 % int4)) triple14) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple14 ((triple13 ((((((triple14) -> (rule4 % int5)) triple14) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is rough.
("Fiona" "is" "rough" "+")
int5