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