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