Bob is green. Erin is blue. Erin is rough. Erin is smart. Gary is blue. Gary is green. Gary is red. All big things are green. If something is green and rough then it is red. All smart things are big.
Bob is green.
("Bob" "is" "green" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is red.
("Gary" "is" "red" "+")
All big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If something is green and rough then it is red.
((("something" "is" "green" "+") ("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
All smart things are big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
Bob is green.
True
1
proof
[(triple1)]
("Bob" "is" "green" "+")
triple1
Erin is not smart.
False
1
inv-proof
[(triple4)]
("Erin" "is" "smart" "-")
triple4
Erin is big.
True
2
proof
[(((triple4) -> rule3))]
("Erin" "is" "big" "+")
((triple4) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not big.
False
2
inv-proof
[(((triple4) -> rule3))]
("Erin" "is" "big" "-")
((triple4) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is green.
True
3
proof
[(((((triple4) -> rule3)) -> rule1))]
("Erin" "is" "green" "+")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is not green.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule1))]
("Erin" "is" "green" "-")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is red.
True
5
proof
[(((((((triple4) -> rule3)) -> rule1) triple3) -> rule2))]
("Erin" "is" "red" "+")
((((((triple4) -> (rule3 % int3))) -> (rule1 % int2)) triple3) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is not red.
False
5
inv-proof
[(((((((triple4) -> rule3)) -> rule1) triple3) -> rule2))]
("Erin" "is" "red" "-")
((((((triple4) -> (rule3 % int3))) -> (rule1 % int2)) triple3) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "big" "-")
Bob is big.
Unknown
rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "big" "+")
Bob is not red.
Unknown
inv-rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "red" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
@0: Bob is green.[(triple1)] Erin is blue.[(triple2)] Erin is rough.[(triple3)] Erin is smart.[(triple4)] Gary is blue.[(triple5)] Gary is green.[(triple6)] Gary is red.[(triple7)] @1: Erin is big.[(((triple4) -> rule3))] @2: Erin is green.[(((((triple4) -> rule3)) -> rule1))] @3: Erin is red.[(((((((triple4) -> rule3)) -> rule1) triple3) -> rule2))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Erin is rough.
("Erin" "is" "rough" "+")
triple3
Erin is smart.
("Erin" "is" "smart" "+")
triple4
Gary is blue.
("Gary" "is" "blue" "+")
triple5
Gary is green.
("Gary" "is" "green" "+")
triple6
Gary is red.
("Gary" "is" "red" "+")
triple7
Erin is big.
("Erin" "is" "big" "+")
((triple4) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((((((triple4) -> (rule3 % int3))) -> (rule1 % int2)) triple3) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3