Bob is big. Bob is red. Bob is smart. Erin is furry. Erin is green. Erin is quiet. Fiona is big. Fiona is furry. Fiona is green. Fiona is smart. Gary is big. Gary is young. All red, quiet things are young. All quiet, big things are furry. If Erin is young and Erin is smart then Erin is big. If something is green and furry then it is red. All big things are green. All quiet, furry things are smart. Quiet, furry things are red. All young, smart things are furry.
Bob is big.
("Bob" "is" "big" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is young.
("Gary" "is" "young" "+")
All red, quiet things are young.
((("something" "is" "red" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
All quiet, big things are furry.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
If Erin is young and Erin is smart then Erin is big.
((("Erin" "is" "young" "+") ("Erin" "is" "smart" "+")) -> ("Erin" "is" "big" "+"))
If something is green and furry then it is red.
((("something" "is" "green" "+") ("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
All big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
All quiet, furry things are smart.
((("something" "is" "quiet" "+") ("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
Quiet, furry things are red.
((("something" "is" "quiet" "+") ("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
All young, smart things are furry.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
Erin is green.
True
1
proof
[(triple5 OR ((((((((triple6 triple4) -> rule7) triple6) -> rule1) ((triple6 triple4) -> rule6)) -> rule3)) -> rule5))]
("Erin" "is" "green" "+")
triple5
((((((((triple6 triple4) -> (rule7 % int5)) triple6) -> (rule1 % int4)) ((triple6 triple4) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is red.
("Erin" "is" "red" "+")
int5
Bob is not red.
False
1
inv-proof
[(triple2)]
("Bob" "is" "red" "-")
triple2
Erin is smart.
True
3
proof
[(((triple6 triple4) -> rule6))]
("Erin" "is" "smart" "+")
((triple6 triple4) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple1) -> rule5))]
("Bob" "is" "green" "-")
((triple1) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Erin is young.
True
5
proof
[(((((triple5 triple4) -> rule4) triple6) -> rule1) OR ((((triple6 triple4) -> rule7) triple6) -> rule1))]
("Erin" "is" "young" "+")
((((triple5 triple4) -> (rule4 % int2)) triple6) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((triple6 triple4) -> (rule7 % int2)) triple6) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is not young.
False
5
inv-proof
[(((((triple5 triple4) -> rule4) triple6) -> rule1) OR ((((triple6 triple4) -> rule7) triple6) -> rule1))]
("Erin" "is" "young" "-")
((((triple5 triple4) -> (rule4 % int2)) triple6) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((triple6 triple4) -> (rule7 % int2)) triple6) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is big.
True
9
proof
[(((((((triple5 triple4) -> rule4) triple6) -> rule1) ((triple6 triple4) -> rule6)) -> rule3) OR ((((((triple6 triple4) -> rule7) triple6) -> rule1) ((triple6 triple4) -> rule6)) -> rule3))]
("Erin" "is" "big" "+")
((((((triple5 triple4) -> (rule4 % int4)) triple6) -> (rule1 % int3)) ((triple6 triple4) -> (rule6 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4
((((((triple6 triple4) -> (rule7 % int4)) triple6) -> (rule1 % int3)) ((triple6 triple4) -> (rule6 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4
Erin is not big.
False
9
inv-proof
[(((((((triple5 triple4) -> rule4) triple6) -> rule1) ((triple6 triple4) -> rule6)) -> rule3) OR ((((((triple6 triple4) -> rule7) triple6) -> rule1) ((triple6 triple4) -> rule6)) -> rule3))]
("Erin" "is" "big" "-")
((((((triple5 triple4) -> (rule4 % int4)) triple6) -> (rule1 % int3)) ((triple6 triple4) -> (rule6 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4
((((((triple6 triple4) -> (rule7 % int4)) triple6) -> (rule1 % int3)) ((triple6 triple4) -> (rule6 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4
Fiona is not young.
Unknown
inv-rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "young" "-")
Gary is red.
Unknown
rconc
[@3: Gary is red.[CWA. Example of deepest failure = (rule4 <- rule8 <- rule6 <- FAIL)]]
("Gary" "is" "red" "+")
Gary is not furry.
Unknown
inv-rconc
[@2: Gary is furry.[CWA. Example of deepest failure = (rule8 <- rule6 <- FAIL)]]
("Gary" "is" "furry" "-")
Bob is furry.
Unknown
rconc
[@2: Bob is furry.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("Bob" "is" "furry" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Bob is big.[(triple1)] Bob is red.[(triple2)] Bob is smart.[(triple3)] Erin is furry.[(triple4)] Erin is green.[(triple5 OR ((((((((triple6 triple4) -> rule7) triple6) -> rule1) ((triple6 triple4) -> rule6)) -> rule3)) -> rule5))] Erin is quiet.[(triple6)] Fiona is big.[(triple7)] Fiona is furry.[(triple8)] Fiona is green.[(triple9 OR ((triple7) -> rule5))] Fiona is smart.[(triple10)] Gary is big.[(triple11)] Gary is young.[(triple12)] @1: Bob is green.[(((triple1) -> rule5))] Erin is red.[(((triple5 triple4) -> rule4) OR ((triple6 triple4) -> rule7))] Erin is smart.[(((triple6 triple4) -> rule6))] Fiona is red.[(((triple9 triple8) -> rule4) OR ((((triple7) -> rule5) triple8) -> rule4))] Gary is green.[(((triple11) -> rule5))] @2: Erin is young.[(((((triple5 triple4) -> rule4) triple6) -> rule1) OR ((((triple6 triple4) -> rule7) triple6) -> rule1))] @3: Erin is big.[(((((((triple5 triple4) -> rule4) triple6) -> rule1) ((triple6 triple4) -> rule6)) -> rule3) OR ((((((triple6 triple4) -> rule7) triple6) -> rule1) ((triple6 triple4) -> rule6)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Erin is furry.
("Erin" "is" "furry" "+")
triple4
Erin is green.
("Erin" "is" "green" "+")
triple5
((((((((triple6 triple4) -> (rule7 % int5)) triple6) -> (rule1 % int4)) ((triple6 triple4) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is red.
("Erin" "is" "red" "+")
int5
Erin is quiet.
("Erin" "is" "quiet" "+")
triple6
Fiona is big.
("Fiona" "is" "big" "+")
triple7
Fiona is furry.
("Fiona" "is" "furry" "+")
triple8
Fiona is green.
("Fiona" "is" "green" "+")
triple9
((triple7) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple10
Gary is big.
("Gary" "is" "big" "+")
triple11
Gary is young.
("Gary" "is" "young" "+")
triple12
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple5 triple4) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple6 triple4) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple6 triple4) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple9 triple8) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((((triple7) -> (rule5 % int2)) triple8) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((triple11) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((((triple5 triple4) -> (rule4 % int2)) triple6) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((triple6 triple4) -> (rule7 % int2)) triple6) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
((((((triple5 triple4) -> (rule4 % int4)) triple6) -> (rule1 % int3)) ((triple6 triple4) -> (rule6 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4
((((((triple6 triple4) -> (rule7 % int4)) triple6) -> (rule1 % int3)) ((triple6 triple4) -> (rule6 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4