Bob is round. Erin is smart. Fiona is smart. Gary is big. If something is round then it is young. If Bob is young then Bob is green. If something is green then it is not smart. If something is young and not blue then it is green. If something is smart and green then it is white. If something is big and smart then it is not round.
Bob is round.
("Bob" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
If something is round then it is young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
If Bob is young then Bob is green.
((("Bob" "is" "young" "+")) -> ("Bob" "is" "green" "+"))
If something is green then it is not smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "-"))
If something is young and not blue then it is green.
((("something" "is" "young" "+") ("something" "is" "blue" "~")) -> ("something" "is" "green" "+"))
If something is smart and green then it is white.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If something is big and smart then it is not round.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "-"))
Gary is big.
True
1
proof
[(triple4)]
("Gary" "is" "big" "+")
triple4
Gary is not big.
False
1
inv-proof
[(triple4)]
("Gary" "is" "big" "-")
triple4
Bob is young.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "young" "+")
((triple1) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not young.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "young" "-")
((triple1) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is green.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("Bob" "is" "green" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is not green.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("Bob" "is" "green" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is not smart.
True
4
proof
[(((((((triple1) -> rule1)) -> rule2)) -> rule3))]
("Bob" "is" "smart" "-")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is smart.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule2)) -> rule3))]
("Bob" "is" "smart" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "green" "-")
Bob is white.
Unknown
rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "white" "+")
Fiona is not green.
Unknown
inv-rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "green" "-")
Erin is white.
Unknown
rconc
[@2: Erin is white.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Erin" "is" "white" "+")
Fiona is not round.
Unknown
inv-random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
@0: Bob is round.[(triple1)] Erin is smart.[(triple2)] Fiona is smart.[(triple3)] Gary is big.[(triple4)] @1: Bob is young.[(((triple1) -> rule1))] @2: Bob is green.[(((((triple1) -> rule1)) -> rule2))] @3: Bob is not smart.[(((((((triple1) -> rule1)) -> rule2)) -> rule3))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
triple2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple3
Gary is big.
("Gary" "is" "big" "+")
triple4
Bob is young.
("Bob" "is" "young" "+")
((triple1) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is not smart.
("Bob" "is" "smart" "-")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3