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