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