Bob is green. Erin is blue. Gary is green. Harry is kind. If something is blue then it is red. Round, red things are green. If Erin is red then Erin is round.
Bob is green.
("Bob" "is" "green" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
If something is blue then it is red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
Round, red things are green.
((("something" "is" "round" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If Erin is red then Erin is round.
((("Erin" "is" "red" "+")) -> ("Erin" "is" "round" "+"))
Bob is green.
True
1
proof
[(triple1)]
("Bob" "is" "green" "+")
triple1
Gary is not green.
False
1
inv-proof
[(triple3)]
("Gary" "is" "green" "-")
triple3
Erin is red.
True
2
proof
[(((triple2) -> rule1))]
("Erin" "is" "red" "+")
((triple2) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is not red.
False
2
inv-proof
[(((triple2) -> rule1))]
("Erin" "is" "red" "-")
((triple2) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("Erin" "is" "round" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is not round.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("Erin" "is" "round" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is green.
True
6
proof
[(((((((triple2) -> rule1)) -> rule3) ((triple2) -> rule1)) -> rule2))]
("Erin" "is" "green" "+")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2)) ((triple2) -> (rule1 % int3))) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is not green.
False
6
inv-proof
[(((((((triple2) -> rule1)) -> rule3) ((triple2) -> rule1)) -> rule2))]
("Erin" "is" "green" "-")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2)) ((triple2) -> (rule1 % int3))) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Bob is not red.
Unknown
inv-rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "red" "-")
Harry is red.
Unknown
rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "red" "+")
Gary is not red.
Unknown
inv-rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "red" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "green" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
@0: Bob is green.[(triple1)] Erin is blue.[(triple2)] Gary is green.[(triple3)] Harry is kind.[(triple4)] @1: Erin is red.[(((triple2) -> rule1))] @2: Erin is round.[(((((triple2) -> rule1)) -> rule3))] @3: Erin is green.[(((((((triple2) -> rule1)) -> rule3) ((triple2) -> rule1)) -> rule2))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Erin is red.
("Erin" "is" "red" "+")
((triple2) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2)) ((triple2) -> (rule1 % int3))) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3