Anne is kind. Anne is nice. Anne is red. Anne is rough. Anne is round. Anne is white. Anne is young. Fiona is round. Fiona is white. Fiona is young. If someone is red and young then they are white. Nice, young people are round. All young people are round. Kind people are rough. White, nice people are red. If Anne is white and Anne is young then Anne is kind. If Fiona is round then Fiona is kind. If Fiona is nice then Fiona is rough.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If someone is red and young then they are white.
((("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
Nice, young people are round.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
All young people are round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
Kind people are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
White, nice people are red.
((("someone" "is" "white" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If Anne is white and Anne is young then Anne is kind.
((("Anne" "is" "white" "+") ("Anne" "is" "young" "+")) -> ("Anne" "is" "kind" "+"))
If Fiona is round then Fiona is kind.
((("Fiona" "is" "round" "+")) -> ("Fiona" "is" "kind" "+"))
If Fiona is nice then Fiona is rough.
((("Fiona" "is" "nice" "+")) -> ("Fiona" "is" "rough" "+"))
Anne is rough.
True
1
proof
[(triple4 OR ((triple1) -> rule4) OR ((((triple6 triple7) -> rule6)) -> rule4) OR ((((((triple3 triple7) -> rule1) triple7) -> rule6)) -> rule4))]
("Anne" "is" "rough" "+")
triple4
((triple1) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((triple6 triple7) -> (rule6 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((((triple3 triple7) -> (rule1 % int3)) triple7) -> (rule6 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is not round.
False
1
inv-proof
[(triple5 OR ((triple7) -> rule3) OR ((triple2 triple7) -> rule2))]
("Anne" "is" "round" "-")
triple5
((triple7) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((triple2 triple7) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Fiona is kind.
True
2
proof
[(((triple8) -> rule7) OR ((((triple10) -> rule3)) -> rule7))]
("Fiona" "is" "kind" "+")
((triple8) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is not kind.
False
2
inv-proof
[(((triple8) -> rule7) OR ((((triple10) -> rule3)) -> rule7))]
("Fiona" "is" "kind" "-")
((triple8) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is not red.
Unknown
inv-rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "red" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
@0: Anne is kind.[(triple1 OR ((triple6 triple7) -> rule6) OR ((((triple3 triple7) -> rule1) triple7) -> rule6))] Anne is nice.[(triple2)] Anne is red.[(triple3 OR ((triple6 triple2) -> rule5))] Anne is rough.[(triple4 OR ((triple1) -> rule4) OR ((((triple6 triple7) -> rule6)) -> rule4) OR ((((((triple3 triple7) -> rule1) triple7) -> rule6)) -> rule4))] Anne is round.[(triple5 OR ((triple7) -> rule3) OR ((triple2 triple7) -> rule2))] Anne is white.[(triple6 OR ((triple3 triple7) -> rule1))] Anne is young.[(triple7)] Fiona is round.[(triple8 OR ((triple10) -> rule3))] Fiona is white.[(triple9)] Fiona is young.[(triple10)] @1: Fiona is kind.[(((triple8) -> rule7) OR ((((triple10) -> rule3)) -> rule7))] @2: Fiona is rough.[(((((triple8) -> rule7)) -> rule4) OR ((((((triple10) -> rule3)) -> rule7)) -> rule4))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
((triple6 triple7) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((triple3 triple7) -> (rule1 % int2)) triple7) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
((triple6 triple2) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
triple4
((triple1) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((triple6 triple7) -> (rule6 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((((triple3 triple7) -> (rule1 % int3)) triple7) -> (rule6 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
triple5
((triple7) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((triple2 triple7) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
triple6
((triple3 triple7) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple7
Fiona is round.
("Fiona" "is" "round" "+")
triple8
((triple10) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
triple9
Fiona is young.
("Fiona" "is" "young" "+")
triple10
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple8) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
((((triple8) -> (rule7 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((((((triple10) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3