Charlie is cold. Charlie is green. Erin is cold. Erin is green. Erin is quiet. Erin is red. Erin is round. Fiona is green. Fiona is kind. Fiona is red. If someone is cold then they are quiet. Kind people are round. Cold, quiet people are kind.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is red.
("Fiona" "is" "red" "+")
If someone is cold then they are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
Kind people are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
Cold, quiet people are kind.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
Fiona is kind.
True
1
proof
[(triple9)]
("Fiona" "is" "kind" "+")
triple9
Fiona is not green.
False
1
inv-proof
[(triple8)]
("Fiona" "is" "green" "-")
triple8
Charlie is quiet.
True
2
proof
[(((triple1) -> rule1))]
("Charlie" "is" "quiet" "+")
((triple1) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple1) -> rule1))]
("Charlie" "is" "quiet" "-")
((triple1) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is kind.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule3))]
("Charlie" "is" "kind" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not kind.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule3))]
("Charlie" "is" "kind" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is round.
True
5
proof
[(((((triple1 ((triple1) -> rule1)) -> rule3)) -> rule2))]
("Charlie" "is" "round" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is not round.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule1)) -> rule3)) -> rule2))]
("Charlie" "is" "round" "-")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Fiona is not quiet.
Unknown
inv-rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
Fiona is not cold.
Unknown
inv-random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
@0: Charlie is cold.[(triple1)] Charlie is green.[(triple2)] Erin is cold.[(triple3)] Erin is green.[(triple4)] Erin is quiet.[(triple5 OR ((triple3) -> rule1))] Erin is red.[(triple6)] Erin is round.[(triple7 OR ((((triple3 triple5) -> rule3)) -> rule2) OR ((((triple3 ((triple3) -> rule1)) -> rule3)) -> rule2))] Fiona is green.[(triple8)] Fiona is kind.[(triple9)] Fiona is red.[(triple10)] @1: Charlie is quiet.[(((triple1) -> rule1))] Erin is kind.[(((triple3 triple5) -> rule3) OR ((triple3 ((triple3) -> rule1)) -> rule3))] Fiona is round.[(((triple9) -> rule2))] @2: Charlie is kind.[(((triple1 ((triple1) -> rule1)) -> rule3))] @3: Charlie is round.[(((((triple1 ((triple1) -> rule1)) -> rule3)) -> rule2))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Erin is green.
("Erin" "is" "green" "+")
triple4
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
((triple3) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
triple6
Erin is round.
("Erin" "is" "round" "+")
triple7
((((triple3 triple5) -> (rule3 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
triple8
Fiona is kind.
("Fiona" "is" "kind" "+")
triple9
Fiona is red.
("Fiona" "is" "red" "+")
triple10
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple3 triple5) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple3 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
((triple9) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3