Bob is rough. Charlie is quiet. Charlie is round. Charlie is smart. Charlie is young. Dave is big. Dave is cold. Dave is quiet. Dave is rough. Dave is round. Dave is smart. Dave is not young. Harry is cold. Harry is round. Harry is smart. Harry is young. Smart people are quiet. All big, young people are quiet. If someone is round then they are smart. All quiet, rough people are round. Smart people are rough. If someone is smart and not round then they are cold.
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is not young.
("Dave" "is" "young" "-")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
Smart people are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
All big, young people are quiet.
((("someone" "is" "big" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
If someone is round then they are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
All quiet, rough people are round.
((("someone" "is" "quiet" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
Smart people are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
If someone is smart and not round then they are cold.
((("someone" "is" "smart" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "cold" "+"))
Dave is smart.
True
1
proof
[(triple11 OR ((triple10) -> rule3) OR ((((triple8 triple9) -> rule4)) -> rule3))]
("Dave" "is" "smart" "+")
triple11
((triple10) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((((triple8 triple9) -> (rule4 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Charlie is not young.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "young" "-")
triple5
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "cold" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is rough.[(triple1)] Charlie is quiet.[(triple2 OR ((triple4) -> rule1) OR ((((triple3) -> rule3)) -> rule1))] Charlie is round.[(triple3 OR ((triple2 ((triple4) -> rule5)) -> rule4) OR ((((triple4) -> rule1) ((triple4) -> rule5)) -> rule4))] Charlie is smart.[(triple4 OR ((triple3) -> rule3))] Charlie is young.[(triple5)] Dave is big.[(triple6)] Dave is cold.[(triple7)] Dave is not young.[(triple12)] Dave is quiet.[(triple8 OR ((triple11) -> rule1) OR ((((triple10) -> rule3)) -> rule1))] Dave is rough.[(triple9 OR ((triple11) -> rule5) OR ((((triple10) -> rule3)) -> rule5))] Dave is round.[(triple10 OR ((triple8 triple9) -> rule4) OR ((triple8 ((triple11) -> rule5)) -> rule4) OR ((((triple11) -> rule1) triple9) -> rule4) OR ((((triple11) -> rule1) ((triple11) -> rule5)) -> rule4))] Dave is smart.[(triple11 OR ((triple10) -> rule3) OR ((((triple8 triple9) -> rule4)) -> rule3))] Harry is cold.[(triple13)] Harry is round.[(triple14 OR ((((triple15) -> rule1) ((triple15) -> rule5)) -> rule4))] Harry is smart.[(triple15 OR ((triple14) -> rule3))] Harry is young.[(triple16)] @1: Charlie is rough.[(((triple4) -> rule5) OR ((((triple3) -> rule3)) -> rule5))] Harry is quiet.[(((triple15) -> rule1) OR ((((triple14) -> rule3)) -> rule1))] Harry is rough.[(((triple15) -> rule5) OR ((((triple14) -> rule3)) -> rule5))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
((triple4) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
((triple2 ((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple4) -> (rule1 % int3)) ((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
((triple3) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Dave is big.
("Dave" "is" "big" "+")
triple6
Dave is cold.
("Dave" "is" "cold" "+")
triple7
Dave is not young.
("Dave" "is" "young" "-")
triple12
Dave is quiet.
("Dave" "is" "quiet" "+")
triple8
((triple11) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
triple9
((triple11) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
triple10
((triple8 triple9) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple8 ((triple11) -> (rule5 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((triple11) -> (rule1 % int2)) triple9) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((triple11) -> (rule1 % int3)) ((triple11) -> (rule5 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
triple11
((triple10) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((((triple8 triple9) -> (rule4 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
triple13
Harry is round.
("Harry" "is" "round" "+")
triple14
((((triple15) -> (rule1 % int3)) ((triple15) -> (rule5 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
triple15
((triple14) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple16
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple4) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple15) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple14) -> (rule3 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((triple15) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple14) -> (rule3 % int2))) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2