Anne is big. Bob is round. Dave is young. Fiona is young. If someone is round then they are young. If someone is big then they are round. If someone is rough then they are round. White, quiet people are young. If someone is young then they are rough. If Bob is blue then Bob is round. If someone is young then they are round. All blue people are big.
Anne is big.
("Anne" "is" "big" "+")
Bob is round.
("Bob" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If someone is round then they are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
If someone is big then they are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If someone is rough then they are round.
((("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
White, quiet people are young.
((("someone" "is" "white" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
If someone is young then they are rough.
((("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
If Bob is blue then Bob is round.
((("Bob" "is" "blue" "+")) -> ("Bob" "is" "round" "+"))
If someone is young then they are round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
All blue people are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Dave is round.
True
2
proof
[(((triple3) -> rule7) OR ((((triple3) -> rule5)) -> rule3))]
("Dave" "is" "round" "+")
((triple3) -> (rule7 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Bob is not young.
False
2
inv-proof
[(((triple2) -> rule1))]
("Bob" "is" "young" "-")
((triple2) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Anne is young.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("Anne" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Bob is not rough.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule5))]
("Bob" "is" "rough" "-")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Anne is rough.
True
4
proof
[(((((((triple1) -> rule2)) -> rule1)) -> rule5))]
("Anne" "is" "rough" "+")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is not rough.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule1)) -> rule5))]
("Anne" "is" "rough" "-")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "big" "-")
Dave is big.
Unknown
rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "big" "+")
Fiona is not big.
Unknown
inv-rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "big" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Anne is big.[(triple1)] Bob is round.[(triple2)] Dave is young.[(triple3)] Fiona is young.[(triple4)] @1: Anne is round.[(((triple1) -> rule2))] Bob is young.[(((triple2) -> rule1))] Dave is rough.[(((triple3) -> rule5))] Dave is round.[(((triple3) -> rule7) OR ((((triple3) -> rule5)) -> rule3))] Fiona is rough.[(((triple4) -> rule5))] Fiona is round.[(((triple4) -> rule7) OR ((((triple4) -> rule5)) -> rule3))] @2: Anne is young.[(((((triple1) -> rule2)) -> rule1))] Bob is rough.[(((((triple2) -> rule1)) -> rule5))] @3: Anne is rough.[(((((((triple1) -> rule2)) -> rule1)) -> rule5))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Dave is young.
("Dave" "is" "young" "+")
triple3
Fiona is young.
("Fiona" "is" "young" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple2) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple3) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple3) -> (rule7 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple4) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((triple4) -> (rule7 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((((triple4) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3