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