Bob is kind. Erin is cold. Gary is round. Harry is young. Cold, young people are red. All young people are cold. If someone is young and kind then they are white. Cold, kind people are red. If Erin is round and Erin is cold then Erin is green. If Bob is white and Bob is red then Bob is green. If someone is cold then they are kind. If someone is red and cold then they are kind.
Bob is kind.
("Bob" "is" "kind" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
Cold, young people are red.
((("someone" "is" "cold" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
All young people are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If someone is young and kind then they are white.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
Cold, kind people are red.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
If Erin is round and Erin is cold then Erin is green.
((("Erin" "is" "round" "+") ("Erin" "is" "cold" "+")) -> ("Erin" "is" "green" "+"))
If Bob is white and Bob is red then Bob is green.
((("Bob" "is" "white" "+") ("Bob" "is" "red" "+")) -> ("Bob" "is" "green" "+"))
If someone is cold then they are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If someone is red and cold then they are kind.
((("someone" "is" "red" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
Bob is kind.
True
1
proof
[(triple1)]
("Bob" "is" "kind" "+")
triple1
Erin is not cold.
False
1
inv-proof
[(triple2)]
("Erin" "is" "cold" "-")
triple2
Erin is kind.
True
2
proof
[(((triple2) -> rule7))]
("Erin" "is" "kind" "+")
((triple2) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple4) -> rule2))]
("Harry" "is" "cold" "-")
((triple4) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is red.
True
4
proof
[(((((triple4) -> rule2) triple4) -> rule1) OR ((((triple4) -> rule2) ((((triple4) -> rule2)) -> rule7)) -> rule4))]
("Harry" "is" "red" "+")
((((triple4) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple4) -> (rule2 % int3)) ((((triple4) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Erin is not red.
False
4
inv-proof
[(((triple2 ((triple2) -> rule7)) -> rule4))]
("Erin" "is" "red" "-")
((triple2 ((triple2) -> (rule7 % int2))) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Harry is white.
True
5
proof
[(((triple4 ((((triple4) -> rule2)) -> rule7)) -> rule3) OR ((triple4 ((((((triple4) -> rule2) triple4) -> rule1) ((triple4) -> rule2)) -> rule8)) -> rule3))]
("Harry" "is" "white" "+")
((triple4 ((((triple4) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
((triple4 ((((((triple4) -> (rule2 % int4)) triple4) -> (rule1 % int3)) ((triple4) -> (rule2 % int4))) -> (rule8 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is not white.
False
5
inv-proof
[(((triple4 ((((triple4) -> rule2)) -> rule7)) -> rule3) OR ((triple4 ((((((triple4) -> rule2) triple4) -> rule1) ((triple4) -> rule2)) -> rule8)) -> rule3))]
("Harry" "is" "white" "-")
((triple4 ((((triple4) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
((triple4 ((((((triple4) -> (rule2 % int4)) triple4) -> (rule1 % int3)) ((triple4) -> (rule2 % int4))) -> (rule8 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Gary is not kind.
Unknown
inv-rconc
[@2: Gary is kind.[CWA. Example of deepest failure = (rule7 <- rule2 <- FAIL)]]
("Gary" "is" "kind" "-")
Bob is red.
Unknown
rconc
[@2: Bob is red.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Bob" "is" "red" "+")
Bob is not green.
Unknown
inv-rconc
[@2: Bob is green.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Bob" "is" "green" "-")
Bob is white.
Unknown
rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "white" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Bob is kind.[(triple1)] Erin is cold.[(triple2)] Gary is round.[(triple3)] Harry is young.[(triple4)] @1: Erin is kind.[(((triple2) -> rule7))] Harry is cold.[(((triple4) -> rule2))] @2: Erin is red.[(((triple2 ((triple2) -> rule7)) -> rule4))] Harry is kind.[(((((triple4) -> rule2)) -> rule7) OR ((((((triple4) -> rule2) triple4) -> rule1) ((triple4) -> rule2)) -> rule8))] Harry is red.[(((((triple4) -> rule2) triple4) -> rule1) OR ((((triple4) -> rule2) ((((triple4) -> rule2)) -> rule7)) -> rule4))] @3: Harry is white.[(((triple4 ((((triple4) -> rule2)) -> rule7)) -> rule3) OR ((triple4 ((((((triple4) -> rule2) triple4) -> rule1) ((triple4) -> rule2)) -> rule8)) -> rule3))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Gary is round.
("Gary" "is" "round" "+")
triple3
Harry is young.
("Harry" "is" "young" "+")
triple4
Erin is kind.
("Erin" "is" "kind" "+")
((triple2) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple4) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple2 ((triple2) -> (rule7 % int2))) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((((triple4) -> (rule2 % int2))) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((((triple4) -> (rule2 % int3)) triple4) -> (rule1 % int2)) ((triple4) -> (rule2 % int3))) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
((((triple4) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple4) -> (rule2 % int3)) ((((triple4) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
((triple4 ((((triple4) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
((triple4 ((((((triple4) -> (rule2 % int4)) triple4) -> (rule1 % int3)) ((triple4) -> (rule2 % int4))) -> (rule8 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4