Bob is green. Bob is round. Charlie is big. Charlie is furry. Charlie is round. Dave is nice. Dave is red. Dave is round. Dave is young. Fiona is nice. Fiona is red. Fiona is not round. If Bob is round and Bob is young then Bob is furry. If something is red then it is furry. Young things are furry. Big things are red. All round, green things are nice. Nice, green things are young. If Fiona is young then Fiona is red. Nice, furry things are big.
Bob is green.
("Bob" "is" "green" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is not round.
("Fiona" "is" "round" "-")
If Bob is round and Bob is young then Bob is furry.
((("Bob" "is" "round" "+") ("Bob" "is" "young" "+")) -> ("Bob" "is" "furry" "+"))
If something is red then it is furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
Young things are furry.
((("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
Big things are red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
All round, green things are nice.
((("something" "is" "round" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
Nice, green things are young.
((("something" "is" "nice" "+") ("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If Fiona is young then Fiona is red.
((("Fiona" "is" "young" "+")) -> ("Fiona" "is" "red" "+"))
Nice, furry things are big.
((("something" "is" "nice" "+") ("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
Dave is young.
True
1
proof
[(triple9)]
("Dave" "is" "young" "+")
triple9
Charlie is not round.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "round" "-")
triple5
Bob is nice.
True
3
proof
[(((triple2 triple1) -> rule5))]
("Bob" "is" "nice" "+")
((triple2 triple1) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not nice.
False
3
inv-proof
[(((triple2 triple1) -> rule5))]
("Bob" "is" "nice" "-")
((triple2 triple1) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Fiona is big.
True
4
proof
[(((triple10 ((triple11) -> rule2)) -> rule8))]
("Fiona" "is" "big" "+")
((triple10 ((triple11) -> (rule2 % int2))) -> (rule8 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is not big.
False
4
inv-proof
[(((triple10 ((triple11) -> rule2)) -> rule8))]
("Fiona" "is" "big" "-")
((triple10 ((triple11) -> (rule2 % int2))) -> (rule8 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Bob is furry.
True
6
proof
[(((((((triple2 triple1) -> rule5) triple1) -> rule6)) -> rule3) OR ((triple2 ((((triple2 triple1) -> rule5) triple1) -> rule6)) -> rule1))]
("Bob" "is" "furry" "+")
((((((triple2 triple1) -> (rule5 % int3)) triple1) -> (rule6 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
((triple2 ((((triple2 triple1) -> (rule5 % int3)) triple1) -> (rule6 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is not furry.
False
6
inv-proof
[(((((((triple2 triple1) -> rule5) triple1) -> rule6)) -> rule3) OR ((triple2 ((((triple2 triple1) -> rule5) triple1) -> rule6)) -> rule1))]
("Bob" "is" "furry" "-")
((((((triple2 triple1) -> (rule5 % int3)) triple1) -> (rule6 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
((triple2 ((((triple2 triple1) -> (rule5 % int3)) triple1) -> (rule6 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is big.
True
10
proof
[(((((triple2 triple1) -> rule5) ((((((triple2 triple1) -> rule5) triple1) -> rule6)) -> rule3)) -> rule8) OR ((((triple2 triple1) -> rule5) ((triple2 ((((triple2 triple1) -> rule5) triple1) -> rule6)) -> rule1)) -> rule8))]
("Bob" "is" "big" "+")
((((triple2 triple1) -> (rule5 % int4)) ((((((triple2 triple1) -> (rule5 % int4)) triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
((((triple2 triple1) -> (rule5 % int4)) ((triple2 ((((triple2 triple1) -> (rule5 % int4)) triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
Bob is not big.
False
10
inv-proof
[(((((triple2 triple1) -> rule5) ((((((triple2 triple1) -> rule5) triple1) -> rule6)) -> rule3)) -> rule8) OR ((((triple2 triple1) -> rule5) ((triple2 ((((triple2 triple1) -> rule5) triple1) -> rule6)) -> rule1)) -> rule8))]
("Bob" "is" "big" "-")
((((triple2 triple1) -> (rule5 % int4)) ((((((triple2 triple1) -> (rule5 % int4)) triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
((((triple2 triple1) -> (rule5 % int4)) ((triple2 ((((triple2 triple1) -> (rule5 % int4)) triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
Bob is red.
True
11
proof
[(((((((triple2 triple1) -> rule5) ((((((triple2 triple1) -> rule5) triple1) -> rule6)) -> rule3)) -> rule8)) -> rule4) OR ((((((triple2 triple1) -> rule5) ((triple2 ((((triple2 triple1) -> rule5) triple1) -> rule6)) -> rule1)) -> rule8)) -> rule4))]
("Bob" "is" "red" "+")
((((((triple2 triple1) -> (rule5 % int5)) ((((((triple2 triple1) -> (rule5 % int5)) triple1) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is nice.
("Bob" "is" "nice" "+")
int5
((((((triple2 triple1) -> (rule5 % int5)) ((triple2 ((((triple2 triple1) -> (rule5 % int5)) triple1) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is nice.
("Bob" "is" "nice" "+")
int5
Bob is not red.
False
11
inv-proof
[(((((((triple2 triple1) -> rule5) ((((((triple2 triple1) -> rule5) triple1) -> rule6)) -> rule3)) -> rule8)) -> rule4) OR ((((((triple2 triple1) -> rule5) ((triple2 ((((triple2 triple1) -> rule5) triple1) -> rule6)) -> rule1)) -> rule8)) -> rule4))]
("Bob" "is" "red" "-")
((((((triple2 triple1) -> (rule5 % int5)) ((((((triple2 triple1) -> (rule5 % int5)) triple1) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is nice.
("Bob" "is" "nice" "+")
int5
((((((triple2 triple1) -> (rule5 % int5)) ((triple2 ((((triple2 triple1) -> (rule5 % int5)) triple1) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is nice.
("Bob" "is" "nice" "+")
int5
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is nice.
Unknown
rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "nice" "+")
Fiona is not young.
Unknown
inv-rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "young" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Bob is green.[(triple1)] Bob is round.[(triple2)] Charlie is big.[(triple3)] Charlie is furry.[(triple4 OR ((((triple3) -> rule4)) -> rule2))] Charlie is round.[(triple5)] Dave is nice.[(triple6)] Dave is red.[(triple7 OR ((((triple6 ((triple9) -> rule3)) -> rule8)) -> rule4))] Dave is round.[(triple8)] Dave is young.[(triple9)] Fiona is nice.[(triple10)] Fiona is not round.[(triple12)] Fiona is red.[(triple11)] @1: Bob is nice.[(((triple2 triple1) -> rule5))] Charlie is red.[(((triple3) -> rule4))] Dave is furry.[(((triple7) -> rule2) OR ((triple9) -> rule3))] Fiona is furry.[(((triple11) -> rule2))] @2: Bob is young.[(((((triple2 triple1) -> rule5) triple1) -> rule6))] Dave is big.[(((triple6 ((triple7) -> rule2)) -> rule8) OR ((triple6 ((triple9) -> rule3)) -> rule8))] Fiona is big.[(((triple10 ((triple11) -> rule2)) -> rule8))] @3: Bob is furry.[(((((((triple2 triple1) -> rule5) triple1) -> rule6)) -> rule3) OR ((triple2 ((((triple2 triple1) -> rule5) triple1) -> rule6)) -> rule1))] @4: Bob is big.[(((((triple2 triple1) -> rule5) ((((((triple2 triple1) -> rule5) triple1) -> rule6)) -> rule3)) -> rule8) OR ((((triple2 triple1) -> rule5) ((triple2 ((((triple2 triple1) -> rule5) triple1) -> rule6)) -> rule1)) -> rule8))] @5: Bob is red.[(((((((triple2 triple1) -> rule5) ((((((triple2 triple1) -> rule5) triple1) -> rule6)) -> rule3)) -> rule8)) -> rule4) OR ((((((triple2 triple1) -> rule5) ((triple2 ((((triple2 triple1) -> rule5) triple1) -> rule6)) -> rule1)) -> rule8)) -> rule4))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
Charlie is furry.
("Charlie" "is" "furry" "+")
triple4
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
triple5
Dave is nice.
("Dave" "is" "nice" "+")
triple6
Dave is red.
("Dave" "is" "red" "+")
triple7
((((triple6 ((triple9) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
triple8
Dave is young.
("Dave" "is" "young" "+")
triple9
Fiona is nice.
("Fiona" "is" "nice" "+")
triple10
Fiona is not round.
("Fiona" "is" "round" "-")
triple12
Fiona is red.
("Fiona" "is" "red" "+")
triple11
Bob is nice.
("Bob" "is" "nice" "+")
((triple2 triple1) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple3) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple7) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple9) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
((triple11) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((((triple2 triple1) -> (rule5 % int2)) triple1) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((triple6 ((triple7) -> (rule2 % int2))) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((triple6 ((triple9) -> (rule3 % int2))) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
((triple10 ((triple11) -> (rule2 % int2))) -> (rule8 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((((((triple2 triple1) -> (rule5 % int3)) triple1) -> (rule6 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
((triple2 ((((triple2 triple1) -> (rule5 % int3)) triple1) -> (rule6 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
((((triple2 triple1) -> (rule5 % int4)) ((((((triple2 triple1) -> (rule5 % int4)) triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
((((triple2 triple1) -> (rule5 % int4)) ((triple2 ((((triple2 triple1) -> (rule5 % int4)) triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
((((((triple2 triple1) -> (rule5 % int5)) ((((((triple2 triple1) -> (rule5 % int5)) triple1) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is nice.
("Bob" "is" "nice" "+")
int5
((((((triple2 triple1) -> (rule5 % int5)) ((triple2 ((((triple2 triple1) -> (rule5 % int5)) triple1) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is nice.
("Bob" "is" "nice" "+")
int5