Bob is young. Erin is green. Fiona is young. If someone is green and round then they are rough. All round people are young. Blue, green people are cold. If someone is big then they are rough. If Fiona is cold then Fiona is big. If Bob is rough then Bob is round. Big people are blue. If Bob is young then Bob is big.
Bob is young.
("Bob" "is" "young" "+")
Erin is green.
("Erin" "is" "green" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If someone is green and round then they are rough.
((("someone" "is" "green" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
All round people are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
Blue, green people are cold.
((("someone" "is" "blue" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
If someone is big then they are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
If Fiona is cold then Fiona is big.
((("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "big" "+"))
If Bob is rough then Bob is round.
((("Bob" "is" "rough" "+")) -> ("Bob" "is" "round" "+"))
Big people are blue.
((("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
If Bob is young then Bob is big.
((("Bob" "is" "young" "+")) -> ("Bob" "is" "big" "+"))
Bob is young.
True
1
proof
[(triple1)]
("Bob" "is" "young" "+")
triple1
Erin is not green.
False
1
inv-proof
[(triple2)]
("Erin" "is" "green" "-")
triple2
Bob is big.
True
2
proof
[(((triple1) -> rule8))]
("Bob" "is" "big" "+")
((triple1) -> (rule8 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is not big.
False
2
inv-proof
[(((triple1) -> rule8))]
("Bob" "is" "big" "-")
((triple1) -> (rule8 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
True
3
proof
[(((((triple1) -> rule8)) -> rule7))]
("Bob" "is" "blue" "+")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not blue.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule7))]
("Bob" "is" "blue" "-")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is round.
True
4
proof
[(((((((triple1) -> rule8)) -> rule4)) -> rule6))]
("Bob" "is" "round" "+")
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is not round.
False
4
inv-proof
[(((((((triple1) -> rule8)) -> rule4)) -> rule6))]
("Bob" "is" "round" "-")
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Fiona is not cold.
Unknown
inv-rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "cold" "-")
Fiona is big.
Unknown
rconc
[@2: Fiona is big.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Fiona" "is" "big" "+")
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "rough" "-")
Fiona is rough.
Unknown
rconc
[@3: Fiona is rough.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule3 <- FAIL)]]
("Fiona" "is" "rough" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Fiona is not green.
Unknown
inv-random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
@0: Bob is young.[(triple1)] Erin is green.[(triple2)] Fiona is young.[(triple3)] @1: Bob is big.[(((triple1) -> rule8))] @2: Bob is blue.[(((((triple1) -> rule8)) -> rule7))] Bob is rough.[(((((triple1) -> rule8)) -> rule4))] @3: Bob is round.[(((((((triple1) -> rule8)) -> rule4)) -> rule6))]
Bob is young.
("Bob" "is" "young" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple2
Fiona is young.
("Fiona" "is" "young" "+")
triple3
Bob is big.
("Bob" "is" "big" "+")
((triple1) -> (rule8 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3