Bob is green. Fiona is young. If something is big then it is furry. If Bob is kind and Bob is green then Bob is young. If something is furry and smart then it is round. All kind things are round. If something is furry then it is young. If something is green then it is big. All smart, green things are young. If something is furry then it is kind.
Bob is green.
("Bob" "is" "green" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If something is big then it is furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
If Bob is kind and Bob is green then Bob is young.
((("Bob" "is" "kind" "+") ("Bob" "is" "green" "+")) -> ("Bob" "is" "young" "+"))
If something is furry and smart then it is round.
((("something" "is" "furry" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
All kind things are round.
((("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
If something is furry then it is young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
If something is green then it is big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
All smart, green things are young.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If something is furry then it is kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
Fiona is young.
True
1
proof
[(triple2)]
("Fiona" "is" "young" "+")
triple2
Fiona is not young.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "young" "-")
triple2
Bob is big.
True
2
proof
[(((triple1) -> rule6))]
("Bob" "is" "big" "+")
((triple1) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is not big.
False
2
inv-proof
[(((triple1) -> rule6))]
("Bob" "is" "big" "-")
((triple1) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
True
3
proof
[(((((triple1) -> rule6)) -> rule1))]
("Bob" "is" "furry" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not furry.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule1))]
("Bob" "is" "furry" "-")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is young.
True
4
proof
[(((((((triple1) -> rule6)) -> rule1)) -> rule5) OR ((((((((triple1) -> rule6)) -> rule1)) -> rule8) triple1) -> rule2))]
("Bob" "is" "young" "+")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((((((triple1) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule8 % int2)) triple1) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is not young.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule1)) -> rule5) OR ((((((((triple1) -> rule6)) -> rule1)) -> rule8) triple1) -> rule2))]
("Bob" "is" "young" "-")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((((((triple1) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule8 % int2)) triple1) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Fiona is not kind.
Unknown
inv-rconc
[@3: Fiona is kind.[CWA. Example of deepest failure = (rule8 <- rule1 <- rule6 <- FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is big.
Unknown
rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "big" "+")
Fiona is not round.
Unknown
inv-rconc
[@4: Fiona is round.[CWA. Example of deepest failure = (rule4 <- rule8 <- rule1 <- rule6 <- FAIL)]]
("Fiona" "is" "round" "-")
Fiona is furry.
Unknown
rconc
[@2: Fiona is furry.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Fiona" "is" "furry" "+")
Fiona is not green.
Unknown
inv-random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Bob is green.[(triple1)] Fiona is young.[(triple2)] @1: Bob is big.[(((triple1) -> rule6))] @2: Bob is furry.[(((((triple1) -> rule6)) -> rule1))] @3: Bob is kind.[(((((((triple1) -> rule6)) -> rule1)) -> rule8))] Bob is young.[(((((((triple1) -> rule6)) -> rule1)) -> rule5) OR ((((((((triple1) -> rule6)) -> rule1)) -> rule8) triple1) -> rule2))] @4: Bob is round.[(((((((((triple1) -> rule6)) -> rule1)) -> rule8)) -> rule4))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Fiona is young.
("Fiona" "is" "young" "+")
triple2
Bob is big.
("Bob" "is" "big" "+")
((triple1) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((((((triple1) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule8 % int2)) triple1) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is round.
("Bob" "is" "round" "+")
((((((((triple1) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4