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