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