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