Anne is furry. Anne is quiet. Dave is cold. Dave is not green. Dave is red. Dave is round. Fiona is furry. Fiona is green. Gary is cold. Gary is round. All smart things are red. If something is cold then it is red. If something is quiet then it is green. Red, furry things are cold. All quiet things are round. If something is smart then it is furry. Furry things are smart. If Fiona is green and Fiona is cold then Fiona is quiet.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is not green.
("Dave" "is" "green" "-")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is round.
("Gary" "is" "round" "+")
All smart things are red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
If something is cold then it is red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If something is quiet then it is green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
Red, furry things are cold.
((("something" "is" "red" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
All quiet things are round.
((("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
If something is smart then it is furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
Furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If Fiona is green and Fiona is cold then Fiona is quiet.
((("Fiona" "is" "green" "+") ("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "quiet" "+"))
Dave is cold.
True
1
proof
[(triple3)]
("Dave" "is" "cold" "+")
triple3
Fiona is not green.
False
1
inv-proof
[(triple8)]
("Fiona" "is" "green" "-")
triple8
Anne is round.
True
2
proof
[(((triple2) -> rule5))]
("Anne" "is" "round" "+")
((triple2) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Gary is not red.
False
2
inv-proof
[(((triple9) -> rule2))]
("Gary" "is" "red" "-")
((triple9) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Anne is red.
True
3
proof
[(((((triple1) -> rule7)) -> rule1))]
("Anne" "is" "red" "+")
((((triple1) -> (rule7 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not red.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule1))]
("Anne" "is" "red" "-")
((((triple1) -> (rule7 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Fiona is cold.
True
5
proof
[(((((((triple7) -> rule7)) -> rule1) triple7) -> rule4))]
("Fiona" "is" "cold" "+")
((((((triple7) -> (rule7 % int3))) -> (rule1 % int2)) triple7) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Anne is not cold.
False
5
inv-proof
[(((((((triple1) -> rule7)) -> rule1) triple1) -> rule4))]
("Anne" "is" "cold" "-")
((((((triple1) -> (rule7 % int3))) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Fiona is quiet.
True
7
proof
[(((triple8 ((((((triple7) -> rule7)) -> rule1) triple7) -> rule4)) -> rule8))]
("Fiona" "is" "quiet" "+")
((triple8 ((((((triple7) -> (rule7 % int4))) -> (rule1 % int3)) triple7) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Fiona is not quiet.
False
7
inv-proof
[(((triple8 ((((((triple7) -> rule7)) -> rule1) triple7) -> rule4)) -> rule8))]
("Fiona" "is" "quiet" "-")
((triple8 ((((((triple7) -> (rule7 % int4))) -> (rule1 % int3)) triple7) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Fiona is round.
True
8
proof
[(((((triple8 ((((((triple7) -> rule7)) -> rule1) triple7) -> rule4)) -> rule8)) -> rule5))]
("Fiona" "is" "round" "+")
((((triple8 ((((((triple7) -> (rule7 % int5))) -> (rule1 % int4)) triple7) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is smart.
("Fiona" "is" "smart" "+")
int5
Fiona is not round.
False
8
inv-proof
[(((((triple8 ((((((triple7) -> rule7)) -> rule1) triple7) -> rule4)) -> rule8)) -> rule5))]
("Fiona" "is" "round" "-")
((((triple8 ((((((triple7) -> (rule7 % int5))) -> (rule1 % int4)) triple7) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is smart.
("Fiona" "is" "smart" "+")
int5
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "green" "-")
Dave is smart.
Unknown
rconc
[@2: Dave is smart.[CWA. Example of deepest failure = (rule7 <- rule6 <- FAIL)]]
("Dave" "is" "smart" "+")
Gary is not smart.
Unknown
inv-rconc
[@2: Gary is smart.[CWA. Example of deepest failure = (rule7 <- rule6 <- FAIL)]]
("Gary" "is" "smart" "-")
Gary is furry.
Unknown
rconc
[@2: Gary is furry.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("Gary" "is" "furry" "+")
Dave is not furry.
Unknown
inv-rconc
[@2: Dave is furry.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("Dave" "is" "furry" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Anne is furry.[(triple1)] Anne is quiet.[(triple2)] Dave is cold.[(triple3)] Dave is not green.[(triple4)] Dave is red.[(triple5 OR ((triple3) -> rule2))] Dave is round.[(triple6)] Fiona is furry.[(triple7)] Fiona is green.[(triple8)] Gary is cold.[(triple9)] Gary is round.[(triple10)] @1: Anne is green.[(((triple2) -> rule3))] Anne is round.[(((triple2) -> rule5))] Anne is smart.[(((triple1) -> rule7))] Fiona is smart.[(((triple7) -> rule7))] Gary is red.[(((triple9) -> rule2))] @2: Anne is red.[(((((triple1) -> rule7)) -> rule1))] Fiona is red.[(((((triple7) -> rule7)) -> rule1))] @3: Anne is cold.[(((((((triple1) -> rule7)) -> rule1) triple1) -> rule4))] Fiona is cold.[(((((((triple7) -> rule7)) -> rule1) triple7) -> rule4))] @4: Fiona is quiet.[(((triple8 ((((((triple7) -> rule7)) -> rule1) triple7) -> rule4)) -> rule8))] @5: Fiona is round.[(((((triple8 ((((((triple7) -> rule7)) -> rule1) triple7) -> rule4)) -> rule8)) -> rule5))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Dave is not green.
("Dave" "is" "green" "-")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
((triple3) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple6
Fiona is furry.
("Fiona" "is" "furry" "+")
triple7
Fiona is green.
("Fiona" "is" "green" "+")
triple8
Gary is cold.
("Gary" "is" "cold" "+")
triple9
Gary is round.
("Gary" "is" "round" "+")
triple10
Anne is green.
("Anne" "is" "green" "+")
((triple2) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((triple2) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple7) -> (rule7 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple9) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule7 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
((((triple7) -> (rule7 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((((((triple1) -> (rule7 % int3))) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
((((((triple7) -> (rule7 % int3))) -> (rule1 % int2)) triple7) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple8 ((((((triple7) -> (rule7 % int4))) -> (rule1 % int3)) triple7) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Fiona is round.
("Fiona" "is" "round" "+")
((((triple8 ((((((triple7) -> (rule7 % int5))) -> (rule1 % int4)) triple7) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is smart.
("Fiona" "is" "smart" "+")
int5