Dave is round. Erin is quiet. If someone is quiet then they are blue. All green people are round. All blue people are green. Cold, quiet people are blue. All round people are blue. Blue, cold people are kind.
Dave is round.
("Dave" "is" "round" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
If someone is quiet then they are blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
All green people are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
All blue people are green.
((("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
Cold, quiet people are blue.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
All round people are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
Blue, cold people are kind.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
Erin is quiet.
True
1
proof
[(triple2)]
("Erin" "is" "quiet" "+")
triple2
Dave is not round.
False
1
inv-proof
[(triple1)]
("Dave" "is" "round" "-")
triple1
Erin is blue.
True
2
proof
[(((triple2) -> rule1))]
("Erin" "is" "blue" "+")
((triple2) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is not blue.
False
2
inv-proof
[(((triple2) -> rule1))]
("Erin" "is" "blue" "-")
((triple2) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Dave is green.
True
3
proof
[(((((triple1) -> rule5)) -> rule3))]
("Dave" "is" "green" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not green.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule3))]
("Dave" "is" "green" "-")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Erin is round.
True
4
proof
[(((((((triple2) -> rule1)) -> rule3)) -> rule2))]
("Erin" "is" "round" "+")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is not round.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule3)) -> rule2))]
("Erin" "is" "round" "-")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is not kind.
Unknown
inv-rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "kind" "-")
Dave is kind.
Unknown
rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "kind" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
@0: Dave is round.[(triple1)] Erin is quiet.[(triple2)] @1: Dave is blue.[(((triple1) -> rule5))] Erin is blue.[(((triple2) -> rule1))] @2: Dave is green.[(((((triple1) -> rule5)) -> rule3))] Erin is green.[(((((triple2) -> rule1)) -> rule3))] @3: Erin is round.[(((((((triple2) -> rule1)) -> rule3)) -> rule2))]
Dave is round.
("Dave" "is" "round" "+")
triple1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
((triple1) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple2) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3