Bob is big. Dave is blue. Erin is nice. If something is big then it is nice. If Erin is green and Erin is furry then Erin is young. Young things are blue. Green things are furry. If Erin is rough and Erin is nice then Erin is green. Nice things are green. If Dave is nice and Dave is young then Dave is blue. If something is young and blue then it is green.
Bob is big.
("Bob" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Erin is nice.
("Erin" "is" "nice" "+")
If something is big then it is nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If Erin is green and Erin is furry then Erin is young.
((("Erin" "is" "green" "+") ("Erin" "is" "furry" "+")) -> ("Erin" "is" "young" "+"))
Young things are blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
Green things are furry.
((("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
If Erin is rough and Erin is nice then Erin is green.
((("Erin" "is" "rough" "+") ("Erin" "is" "nice" "+")) -> ("Erin" "is" "green" "+"))
Nice things are green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If Dave is nice and Dave is young then Dave is blue.
((("Dave" "is" "nice" "+") ("Dave" "is" "young" "+")) -> ("Dave" "is" "blue" "+"))
If something is young and blue then it is green.
((("something" "is" "young" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Erin is not nice.
False
1
inv-proof
[(triple3)]
("Erin" "is" "nice" "-")
triple3
Erin is green.
True
2
proof
[(((triple3) -> rule6))]
("Erin" "is" "green" "+")
((triple3) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple3) -> rule6))]
("Erin" "is" "green" "-")
((triple3) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Bob is green.
True
3
proof
[(((((triple1) -> rule1)) -> rule6))]
("Bob" "is" "green" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Erin is not furry.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule4))]
("Erin" "is" "furry" "-")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "nice" "-")
Bob is blue.
Unknown
rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "blue" "+")
Dave is not green.
Unknown
inv-rconc
[@2: Dave is green.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Dave" "is" "green" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Bob is big.[(triple1)] Dave is blue.[(triple2)] Erin is nice.[(triple3)] @1: Bob is nice.[(((triple1) -> rule1))] Erin is green.[(((triple3) -> rule6))] @2: Bob is green.[(((((triple1) -> rule1)) -> rule6))] Erin is furry.[(((((triple3) -> rule6)) -> rule4))] @3: Bob is furry.[(((((((triple1) -> rule1)) -> rule6)) -> rule4))] Erin is young.[(((((triple3) -> rule6) ((((triple3) -> rule6)) -> rule4)) -> rule2))] @4: Erin is blue.[(((((((triple3) -> rule6) ((((triple3) -> rule6)) -> rule4)) -> rule2)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Erin is nice.
("Erin" "is" "nice" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple3) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
((((triple3) -> (rule6 % int3)) ((((triple3) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
((((((triple3) -> (rule6 % int4)) ((((triple3) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4