Dave is red. Dave is smart. Dave is young. Erin is cold. Erin is green. Erin is red. Erin is young. Harry is red. Harry is rough. Harry is round. Harry is smart. Harry is young. Round, young things are rough. Cold, round things are green. All green things are cold. All rough things are smart. All rough, young things are smart. Cold things are rough.
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
Round, young things are rough.
((("something" "is" "round" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
Cold, round things are green.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
All green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
All rough things are smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
All rough, young things are smart.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
Cold things are rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
Erin is cold.
True
1
proof
[(triple4 OR ((triple5) -> rule3))]
("Erin" "is" "cold" "+")
triple4
((triple5) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not red.
False
1
inv-proof
[(triple6)]
("Erin" "is" "red" "-")
triple6
Erin is rough.
True
2
proof
[(((triple4) -> rule6) OR ((((triple5) -> rule3)) -> rule6))]
("Erin" "is" "rough" "+")
((triple4) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is not rough.
False
2
inv-proof
[(((triple4) -> rule6) OR ((((triple5) -> rule3)) -> rule6))]
("Erin" "is" "rough" "-")
((triple4) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is smart.
True
3
proof
[(((((triple4) -> rule6)) -> rule4) OR ((((triple4) -> rule6) triple7) -> rule5) OR ((((((triple5) -> rule3)) -> rule6)) -> rule4) OR ((((((triple5) -> rule3)) -> rule6) triple7) -> rule5))]
("Erin" "is" "smart" "+")
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((triple4) -> (rule6 % int2)) triple7) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((((triple5) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((((triple5) -> (rule3 % int3))) -> (rule6 % int2)) triple7) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is not smart.
False
3
inv-proof
[(((((triple4) -> rule6)) -> rule4) OR ((((triple4) -> rule6) triple7) -> rule5) OR ((((((triple5) -> rule3)) -> rule6)) -> rule4) OR ((((((triple5) -> rule3)) -> rule6) triple7) -> rule5))]
("Erin" "is" "smart" "-")
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((triple4) -> (rule6 % int2)) triple7) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((((triple5) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((((triple5) -> (rule3 % int3))) -> (rule6 % int2)) triple7) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Harry is not green.
Unknown
inv-rconc
[@2: Harry is green.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Harry" "is" "green" "-")
Dave is cold.
Unknown
rconc
[@2: Dave is cold.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Dave" "is" "cold" "+")
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "green" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Dave is red.[(triple1)] Dave is smart.[(triple2)] Dave is young.[(triple3)] Erin is cold.[(triple4 OR ((triple5) -> rule3))] Erin is green.[(triple5)] Erin is red.[(triple6)] Erin is young.[(triple7)] Harry is red.[(triple8)] Harry is rough.[(triple9 OR ((triple10 triple12) -> rule1))] Harry is round.[(triple10)] Harry is smart.[(triple11 OR ((triple9) -> rule4) OR ((triple9 triple12) -> rule5) OR ((((triple10 triple12) -> rule1)) -> rule4) OR ((((triple10 triple12) -> rule1) triple12) -> rule5))] Harry is young.[(triple12)] @1: Erin is rough.[(((triple4) -> rule6) OR ((((triple5) -> rule3)) -> rule6))] @2: Erin is smart.[(((((triple4) -> rule6)) -> rule4) OR ((((triple4) -> rule6) triple7) -> rule5) OR ((((((triple5) -> rule3)) -> rule6)) -> rule4) OR ((((((triple5) -> rule3)) -> rule6) triple7) -> rule5))]
Dave is red.
("Dave" "is" "red" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Dave is young.
("Dave" "is" "young" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
triple4
((triple5) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple5
Erin is red.
("Erin" "is" "red" "+")
triple6
Erin is young.
("Erin" "is" "young" "+")
triple7
Harry is red.
("Harry" "is" "red" "+")
triple8
Harry is rough.
("Harry" "is" "rough" "+")
triple9
((triple10 triple12) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple10
Harry is smart.
("Harry" "is" "smart" "+")
triple11
((triple9) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((triple9 triple12) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple10 triple12) -> (rule1 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple10 triple12) -> (rule1 % int2)) triple12) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
triple12
Erin is rough.
("Erin" "is" "rough" "+")
((triple4) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((triple4) -> (rule6 % int2)) triple7) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((((triple5) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((((triple5) -> (rule3 % int3))) -> (rule6 % int2)) triple7) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3