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