Charlie is big. Charlie is cold. Charlie is nice. Charlie is rough. Dave is cold. Dave is smart. Erin is cold. Erin is kind. Harry is kind. Harry is smart. If Charlie is rough then Charlie is big. Smart things are big. All kind things are green. If something is big then it is nice. If Charlie is rough then Charlie is big. All green, kind things are nice.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Charlie is rough then Charlie is big.
((("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "big" "+"))
Smart things are big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
All kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
If something is big then it is nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If Charlie is rough then Charlie is big.
((("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "big" "+"))
All green, kind things are nice.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
Harry is smart.
True
1
proof
[(triple10)]
("Harry" "is" "smart" "+")
triple10
Harry is not kind.
False
1
inv-proof
[(triple9)]
("Harry" "is" "kind" "-")
triple9
Harry is big.
True
2
proof
[(((triple10) -> rule2))]
("Harry" "is" "big" "+")
((triple10) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple8) -> rule3))]
("Erin" "is" "green" "-")
((triple8) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is nice.
True
4
proof
[(((((triple8) -> rule3) triple8) -> rule6))]
("Erin" "is" "nice" "+")
((((triple8) -> (rule3 % int2)) triple8) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Dave is not nice.
False
3
inv-proof
[(((((triple6) -> rule2)) -> rule4))]
("Dave" "is" "nice" "-")
((((triple6) -> (rule2 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "green" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "green" "+")
Erin is not big.
Unknown
inv-rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "big" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Charlie is big.[(triple1 OR ((triple4) -> rule1) OR ((triple4) -> rule5))] Charlie is cold.[(triple2)] Charlie is nice.[(triple3 OR ((triple1) -> rule4) OR ((((triple4) -> rule1)) -> rule4) OR ((((triple4) -> rule5)) -> rule4))] Charlie is rough.[(triple4)] Dave is cold.[(triple5)] Dave is smart.[(triple6)] Erin is cold.[(triple7)] Erin is kind.[(triple8)] Harry is kind.[(triple9)] Harry is smart.[(triple10)] @1: Dave is big.[(((triple6) -> rule2))] Erin is green.[(((triple8) -> rule3))] Harry is big.[(((triple10) -> rule2))] Harry is green.[(((triple9) -> rule3))] @2: Dave is nice.[(((((triple6) -> rule2)) -> rule4))] Erin is nice.[(((((triple8) -> rule3) triple8) -> rule6))] Harry is nice.[(((((triple10) -> rule2)) -> rule4) OR ((((triple9) -> rule3) triple9) -> rule6))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple4) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple4) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
((triple1) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
Dave is cold.
("Dave" "is" "cold" "+")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Erin is cold.
("Erin" "is" "cold" "+")
triple7
Erin is kind.
("Erin" "is" "kind" "+")
triple8
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is smart.
("Harry" "is" "smart" "+")
triple10
Dave is big.
("Dave" "is" "big" "+")
((triple6) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple8) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple10) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple9) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((((triple6) -> (rule2 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((triple8) -> (rule3 % int2)) triple8) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((triple10) -> (rule2 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((((triple9) -> (rule3 % int2)) triple9) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2