Dave is green. Dave is quiet. Dave is round. Erin is not cold. Erin is not quiet. Erin is red. Erin is smart. Fiona is not cold. Fiona is green. Fiona is quiet. Fiona is round. Fiona is smart. If Erin is green and Erin is cold then Erin is round. If Erin is smart and Erin is not green then Erin is not red. If Fiona is green then Fiona is not cold. Cold people are round. If Fiona is quiet and Fiona is not cold then Fiona is kind. All red people are not quiet. If Erin is not round then Erin is quiet. Green, kind people are not red.
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Erin is not cold.
("Erin" "is" "cold" "-")
Erin is not quiet.
("Erin" "is" "quiet" "-")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is not cold.
("Fiona" "is" "cold" "-")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
If Erin is green and Erin is cold then Erin is round.
((("Erin" "is" "green" "+") ("Erin" "is" "cold" "+")) -> ("Erin" "is" "round" "+"))
If Erin is smart and Erin is not green then Erin is not red.
((("Erin" "is" "smart" "+") ("Erin" "is" "green" "~")) -> ("Erin" "is" "red" "-"))
If Fiona is green then Fiona is not cold.
((("Fiona" "is" "green" "+")) -> ("Fiona" "is" "cold" "-"))
Cold people are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If Fiona is quiet and Fiona is not cold then Fiona is kind.
((("Fiona" "is" "quiet" "+") ("Fiona" "is" "cold" "~")) -> ("Fiona" "is" "kind" "+"))
All red people are not quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "-"))
If Erin is not round then Erin is quiet.
((("Erin" "is" "round" "~")) -> ("Erin" "is" "quiet" "+"))
Green, kind people are not red.
((("someone" "is" "green" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "-"))
Dave is round.
True
1
proof
[(triple3)]
("Dave" "is" "round" "+")
triple3
Fiona is not quiet.
False
1
inv-proof
[(triple10)]
("Fiona" "is" "quiet" "-")
triple10
Fiona is kind.
True
3
proof
[(((triple10 triple8) -> rule5) OR ((triple10 ((triple9) -> rule3)) -> rule5))]
("Fiona" "is" "kind" "+")
((triple10 triple8) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((triple10 ((triple9) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is not cold.
("Fiona" "is" "cold" "-")
int2
Fiona is not kind.
False
3
inv-proof
[(((triple10 triple8) -> rule5) OR ((triple10 ((triple9) -> rule3)) -> rule5))]
("Fiona" "is" "kind" "-")
((triple10 triple8) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((triple10 ((triple9) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is not cold.
("Fiona" "is" "cold" "-")
int2
Fiona is not red.
True
5
proof
[(((triple9 ((triple10 triple8) -> rule5)) -> rule8) OR ((triple9 ((triple10 ((triple9) -> rule3)) -> rule5)) -> rule8))]
("Fiona" "is" "red" "-")
((triple9 ((triple10 triple8) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((triple9 ((triple10 ((triple9) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is not cold.
("Fiona" "is" "cold" "-")
int3
Fiona is red.
False
5
inv-proof
[(((triple9 ((triple10 triple8) -> rule5)) -> rule8) OR ((triple9 ((triple10 ((triple9) -> rule3)) -> rule5)) -> rule8))]
("Fiona" "is" "red" "+")
((triple9 ((triple10 triple8) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((triple9 ((triple10 ((triple9) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is not cold.
("Fiona" "is" "cold" "-")
int3
Erin is not round.
Unknown
inv-rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "round" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Dave is green.[(triple1)] Dave is quiet.[(triple2)] Dave is round.[(triple3)] Erin is not cold.[(triple4)] Erin is not quiet.[(triple5 OR ((triple6) -> rule6))] Erin is red.[(triple6)] Erin is smart.[(triple7)] Fiona is green.[(triple9)] Fiona is not cold.[(triple8 OR ((triple9) -> rule3))] Fiona is quiet.[(triple10)] Fiona is round.[(triple11)] Fiona is smart.[(triple12)] @1: Fiona is kind.[(((triple10 triple8) -> rule5) OR ((triple10 ((triple9) -> rule3)) -> rule5))] @2: Fiona is not red.[(((triple9 ((triple10 triple8) -> rule5)) -> rule8) OR ((triple9 ((triple10 ((triple9) -> rule3)) -> rule5)) -> rule8))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
Erin is not cold.
("Erin" "is" "cold" "-")
triple4
Erin is not quiet.
("Erin" "is" "quiet" "-")
triple5
((triple6) -> (rule6 % int1))
Erin is not quiet.
("Erin" "is" "quiet" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
triple6
Erin is smart.
("Erin" "is" "smart" "+")
triple7
Fiona is green.
("Fiona" "is" "green" "+")
triple9
Fiona is not cold.
("Fiona" "is" "cold" "-")
triple8
((triple9) -> (rule3 % int1))
Fiona is not cold.
("Fiona" "is" "cold" "-")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple10
Fiona is round.
("Fiona" "is" "round" "+")
triple11
Fiona is smart.
("Fiona" "is" "smart" "+")
triple12
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple10 triple8) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((triple10 ((triple9) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is not cold.
("Fiona" "is" "cold" "-")
int2
Fiona is not red.
("Fiona" "is" "red" "-")
((triple9 ((triple10 triple8) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((triple9 ((triple10 ((triple9) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is not cold.
("Fiona" "is" "cold" "-")
int3