Bob is furry. Bob is kind. Bob is round. Erin is furry. Erin is kind. Erin is round. Erin is smart. Erin is young. Fiona is young. Gary is cold. Gary is round. Gary is white. If Bob is kind and Bob is round then Bob is young. All white, kind people are young. If someone is furry and cold then they are smart. Young, furry people are white. All furry, smart people are kind. Furry, white people are cold. All smart, furry people are young. If someone is furry and kind then they are smart.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is round.
("Bob" "is" "round" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
If Bob is kind and Bob is round then Bob is young.
((("Bob" "is" "kind" "+") ("Bob" "is" "round" "+")) -> ("Bob" "is" "young" "+"))
All white, kind people are young.
((("someone" "is" "white" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
If someone is furry and cold then they are smart.
((("someone" "is" "furry" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
Young, furry people are white.
((("someone" "is" "young" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
All furry, smart people are kind.
((("someone" "is" "furry" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
Furry, white people are cold.
((("someone" "is" "furry" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
All smart, furry people are young.
((("someone" "is" "smart" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
If someone is furry and kind then they are smart.
((("someone" "is" "furry" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
Gary is round.
True
1
proof
[(triple11)]
("Gary" "is" "round" "+")
triple11
Bob is not round.
False
1
inv-proof
[(triple3)]
("Bob" "is" "round" "-")
triple3
Erin is white.
True
3
proof
[(((triple8 triple4) -> rule4) OR ((((triple7 triple4) -> rule7) triple4) -> rule4) OR ((((((triple4 triple5) -> rule8) triple4) -> rule7) triple4) -> rule4))]
("Erin" "is" "white" "+")
((triple8 triple4) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple7 triple4) -> (rule7 % int2)) triple4) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((((triple4 triple5) -> (rule8 % int3)) triple4) -> (rule7 % int2)) triple4) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Bob is not smart.
False
3
inv-proof
[(((triple1 triple2) -> rule8) OR ((triple1 ((triple1 ((((triple2 triple3) -> rule1) triple1) -> rule4)) -> rule6)) -> rule3))]
("Bob" "is" "smart" "-")
((triple1 triple2) -> (rule8 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple1 ((triple1 ((((triple2 triple3) -> (rule1 % int4)) triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is white.
True
5
proof
[(((((triple2 triple3) -> rule1) triple1) -> rule4) OR ((((((triple1 triple2) -> rule8) triple1) -> rule7) triple1) -> rule4))]
("Bob" "is" "white" "+")
((((triple2 triple3) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((((triple1 triple2) -> (rule8 % int3)) triple1) -> (rule7 % int2)) triple1) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Erin is not cold.
False
5
inv-proof
[(((triple4 ((triple8 triple4) -> rule4)) -> rule6) OR ((triple4 ((((triple7 triple4) -> rule7) triple4) -> rule4)) -> rule6) OR ((triple4 ((((((triple4 triple5) -> rule8) triple4) -> rule7) triple4) -> rule4)) -> rule6))]
("Erin" "is" "cold" "-")
((triple4 ((triple8 triple4) -> (rule4 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((triple4 ((((triple7 triple4) -> (rule7 % int3)) triple4) -> (rule4 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
((triple4 ((((((triple4 triple5) -> (rule8 % int4)) triple4) -> (rule7 % int3)) triple4) -> (rule4 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Bob is cold.
True
7
proof
[(((triple1 ((((triple2 triple3) -> rule1) triple1) -> rule4)) -> rule6) OR ((triple1 ((((((triple1 triple2) -> rule8) triple1) -> rule7) triple1) -> rule4)) -> rule6))]
("Bob" "is" "cold" "+")
((triple1 ((((triple2 triple3) -> (rule1 % int3)) triple1) -> (rule4 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
((triple1 ((((((triple1 triple2) -> (rule8 % int4)) triple1) -> (rule7 % int3)) triple1) -> (rule4 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is not cold.
False
7
inv-proof
[(((triple1 ((((triple2 triple3) -> rule1) triple1) -> rule4)) -> rule6) OR ((triple1 ((((((triple1 triple2) -> rule8) triple1) -> rule7) triple1) -> rule4)) -> rule6))]
("Bob" "is" "cold" "-")
((triple1 ((((triple2 triple3) -> (rule1 % int3)) triple1) -> (rule4 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
((triple1 ((((((triple1 triple2) -> (rule8 % int4)) triple1) -> (rule7 % int3)) triple1) -> (rule4 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Fiona is not white.
Unknown
inv-rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "white" "-")
Gary is smart.
Unknown
rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "smart" "+")
Fiona is not smart.
Unknown
inv-rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "smart" "-")
Gary is kind.
Unknown
rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "kind" "+")
Fiona is not round.
Unknown
inv-random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Bob is furry.[(triple1)] Bob is kind.[(triple2)] Bob is round.[(triple3)] Erin is furry.[(triple4)] Erin is kind.[(triple5 OR ((triple4 triple7) -> rule5) OR ((triple4 ((triple4 ((triple4 ((triple8 triple4) -> rule4)) -> rule6)) -> rule3)) -> rule5))] Erin is round.[(triple6)] Erin is smart.[(triple7 OR ((triple4 triple5) -> rule8) OR ((triple4 ((triple4 ((triple8 triple4) -> rule4)) -> rule6)) -> rule3))] Erin is young.[(triple8 OR ((triple7 triple4) -> rule7) OR ((((triple4 triple5) -> rule8) triple4) -> rule7))] Fiona is young.[(triple9)] Gary is cold.[(triple10)] Gary is round.[(triple11)] Gary is white.[(triple12)] @1: Bob is smart.[(((triple1 triple2) -> rule8) OR ((triple1 ((triple1 ((((triple2 triple3) -> rule1) triple1) -> rule4)) -> rule6)) -> rule3))] Bob is young.[(((triple2 triple3) -> rule1) OR ((((triple1 triple2) -> rule8) triple1) -> rule7))] Erin is white.[(((triple8 triple4) -> rule4) OR ((((triple7 triple4) -> rule7) triple4) -> rule4) OR ((((((triple4 triple5) -> rule8) triple4) -> rule7) triple4) -> rule4))] @2: Bob is white.[(((((triple2 triple3) -> rule1) triple1) -> rule4) OR ((((((triple1 triple2) -> rule8) triple1) -> rule7) triple1) -> rule4))] Erin is cold.[(((triple4 ((triple8 triple4) -> rule4)) -> rule6) OR ((triple4 ((((triple7 triple4) -> rule7) triple4) -> rule4)) -> rule6) OR ((triple4 ((((((triple4 triple5) -> rule8) triple4) -> rule7) triple4) -> rule4)) -> rule6))] @3: Bob is cold.[(((triple1 ((((triple2 triple3) -> rule1) triple1) -> rule4)) -> rule6) OR ((triple1 ((((((triple1 triple2) -> rule8) triple1) -> rule7) triple1) -> rule4)) -> rule6))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Erin is furry.
("Erin" "is" "furry" "+")
triple4
Erin is kind.
("Erin" "is" "kind" "+")
triple5
((triple4 triple7) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple4 ((triple4 ((triple4 ((triple8 triple4) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Erin is round.
("Erin" "is" "round" "+")
triple6
Erin is smart.
("Erin" "is" "smart" "+")
triple7
((triple4 triple5) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple4 ((triple4 ((triple8 triple4) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
triple8
((triple7 triple4) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple4 triple5) -> (rule8 % int2)) triple4) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
triple9
Gary is cold.
("Gary" "is" "cold" "+")
triple10
Gary is round.
("Gary" "is" "round" "+")
triple11
Gary is white.
("Gary" "is" "white" "+")
triple12
Bob is smart.
("Bob" "is" "smart" "+")
((triple1 triple2) -> (rule8 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple1 ((triple1 ((((triple2 triple3) -> (rule1 % int4)) triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is young.
("Bob" "is" "young" "+")
((triple2 triple3) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((((triple1 triple2) -> (rule8 % int2)) triple1) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((triple8 triple4) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple7 triple4) -> (rule7 % int2)) triple4) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((((triple4 triple5) -> (rule8 % int3)) triple4) -> (rule7 % int2)) triple4) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
((((triple2 triple3) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((((triple1 triple2) -> (rule8 % int3)) triple1) -> (rule7 % int2)) triple1) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
((triple4 ((triple8 triple4) -> (rule4 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((triple4 ((((triple7 triple4) -> (rule7 % int3)) triple4) -> (rule4 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
((triple4 ((((((triple4 triple5) -> (rule8 % int4)) triple4) -> (rule7 % int3)) triple4) -> (rule4 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Bob is cold.
("Bob" "is" "cold" "+")
((triple1 ((((triple2 triple3) -> (rule1 % int3)) triple1) -> (rule4 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
((triple1 ((((((triple1 triple2) -> (rule8 % int4)) triple1) -> (rule7 % int3)) triple1) -> (rule4 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4