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